PROGRAMOWANIE W JĘZYKU LOGIKI – WPROWADZENIE
LOGIKA PIERWSZEGO RZĘDU
Symbole języka pierwszego rzędu. dzielą się na:
a) symbole logiczne (wspólne dla wszystkich języków)
– zmienne przedmiotowe: x, y, z, …
– stałe logiczne:
¬ ∧ ∨ → ↔ ∀ ∃
, , ,
,
,
,
– symbole techniczne: ( , )
b) symbole pozalogiczne (zależne od języka)
– symbole relacyjne: P, Q, R, …
– symbole funkcyjne: f, g, h, …
– stałe przedmiotowe: a, b, c, …
(Symbole pozalogiczne całkowicie określają dany język)
Językiem pierwszego rzędu
nazywamy układ
(
)
L
L
L
L
Con
Fun
l
L
ρ
;
;
;
Re
=
taki, że
–
Re l
L
jest niepustym zbiorem (symboli relacyjnych),
–
Fun
L
jest zbiorem (symboli funkcyjnych),
–
Con
L
jest zbiorem (stałych przedmiotowych),
przy czym zbiory
Re l
L
,
Fun
L
i
Con
L
są rozłączne, natomiast
ρ
L
jest funkcją, która każdemu
symbolowi relacyjnemu i funkcyjnemu przyporządkowuje dodatnią liczbę całkowitą, zwaną
arnością tego symbolu.
Wyróżniamy dwie klasy
wyrażeń sensownych
języka
L
:
a)
termy
– wyrażenia nazwowe,
b)
formuły
– wyrażenia zdaniowe.
Termami
języka
L
nazywamy wyrażenia języka
L
określone przez następujące warunki
indukcyjne:
– wszystkie zmienne i stałe przedmiotowe są termami ,
–
(
)
n
t
t
f
,
,
1
K
jest termem, jeżeli
f
Fun
L
∈
,
( )
ρ
L
f
n
=
oraz
n
t
t
,
,
1
K
są tremami.
Formułami atomowymi
języka
L
nazywamy wyrażenia
(
)
n
t
t
R
,
,
1
K
,
takie że
R
l
L
∈Re
,
( )
ρ
L
R
n
=
a
n
t
t
,
,
1
K
są tremami języka
L
.
Formułami
języka
L
nazywamy wyrażenia języka
L
określone przez następujące warunki
indukcyjne:
– wszystkie formuły atomowe są formułami,
– jeżeli
A
,
B
są formułami, to wyrażenia
( )
¬A
,
(
)
A
B
∧
,
(
)
A
B
∨
,
(
)
A
B
→
,
(
)
A
B
↔
są formułami,
– jeżeli
A
jest formułą i
x
jest zmienną przedmiotową, to wyrażenia
(
)
∀x A
i
( )
∃x A
są formułami.
KLAUZULE
Literał pozytywny
– formuła atomowa (krótko: atom)
Literał negatywny
– negacja atomu
Literał
– literał pozytywny lub negatywny
Klauzula
– formuła postaci
(
)
n
L
L
L
∨
∨
∨
∀
K
2
1
, gdzie
n
i
L
i
,
,
2
,
1
,
K
=
są literałami.
Przykład klauzuli:
( )
( ) ( )
(
)
(
)
a
y
h
x
f
Q
y
x
P
y
x
,
,
,
∨
∀
∀
Klauzula postaci:
(
)
m
k
B
B
A
A
¬
∨
∨
¬
∨
∨
∨
∀
K
K
1
1
jest równoważna formule
(
) (
)
(
)
m
k
B
B
A
A
∧
∧
¬
∨
∨
∨
∀
K
K
1
1
,
która z kolei jest równoważna formule
(
)
k
m
A
A
B
B
∨
∨
→
∧
∧
∀
K
K
1
1
.
Formułę tę zapisujemy w postaci:
4
3
4
2
1
K
4
3
4
2
1
K
przeslanka
m
wniosek
k
B
B
A
A
,
,
,
,
1
1
←
,
przecinki w przesłance (poprzednik implikacji) oznaczają koniunkcje,
przecinki we wniosku (następnik implikacji) oznaczają alternatywy.
Przykład:
klauzula:
( )
( )
(
)
B
y
Q
A
x
P
y
x
∨
¬
∨
¬
∨
∀
∀
zapis:
( )
( )
y
Q
A
B
x
P
,
,
←
Szczególne przypadki klauzul:
1
=
k
Wtedy klauzula jest postaci:
m
B
B
A
,
,
1
K
←
Klauzulę tej postaci nazywamy klauzula
definitywną
.
W szczególności
0
=
m
.
Wtedy po prawej stronie otrzymujemy pustą koniunkcję (brak przesłanek).
Pusta koniunkcja jest zawsze prawdziwa.
Zatem w tym przypadku klauzula jest postaci:
←
A
Prawda
Klauzulę taką nazywamy
jednostkową
.
0
,
0
>
= m
k
.
Wtedy po prawej stronie otrzymujemy pustą alternatywę (brak wniosków).
Pusta alternatywa jest zawsze fałszywa.
Zatem w tym przypadku klauzula jest postaci:
Fałsz
m
B
B
,
,
1
K
←
Klauzulę taką nazywamy
negatywną
.
0
,
0
=
= m
k
.
Wtedy zarówno koniunkcja jak i alternatywa są puste.
Mamy następującą sytuację :
Fałsz
←
Prawda
Zatem w tym przypadku klauzula jest fałszywa.
Nazywamy ja klauzulą
pustą
i oznaczamy
Program w języku logiki.
Programem w języku logiki nazywamy zbiór klauzul postaci:
m
B
B
A
,
,
1
K
←
,
0
≥
n
nagłówek treść, ciało
tzn. klauzul definitywnych (reguł) (
0
>
n
) i klauzul jednostkowych, czyli faktów (
0
=
n
).
Nieformalne znaczenie klauzuli definitywnej
: dla każdego wartościowania zmiennych,
jeżeli
m
i
B
i
,
,
2
,
1
,
K
=
są prawdziwe, to A jest prawdziwe.
Nieformalne znaczenie klauzuli jednostkowej
: A jest prawdziwe dla każdego
wartościowania zmiennych.
Interpretacja
klauzul programu w języku logiki:
m
B
B
A
,
,
1
K
←
,
0
≥
n
a)
deklaratywna (opisowa):
A
jest prawdziwe, jeśli
m
B
B
,
,
1
K
są prawdziwe,
b)
proceduralna (operacyjna): aby rozwiązać
A
rozwiąż
m
B
B
,
,
1
K
.
Definicją predykatu
(relacji, związku, własności)
n
P /
(predykat
P
o
n
argumentach) w
programie w języku logiki
P
nazywamy zbiór wszystkich klauzul, w których nagłówku
występuje
n
P /
.
Program
P
w języku logiki jest opisem obiektów koniecznych do rozwiązania danego
zagadnienia oraz związków jakie zachodzą pomiędzy tymi obiektami.
Program P w języku logiki jednoznacznie określa język pierwszego rzędu
P
L
.
Zadanie do rozwiązania przedstawione jest w postaci tzw.
celu
(ang. goal),
zapytania.
Zapytanie
jest to klauzula negatywna
N
, taka że
P
L
N
∈
.
Wykonanie programu
polega na udowodnieniu, że podany cel wynika logicznie ze zbioru
formuł tworzących program
P
.
W praktyce wykazujemy, że zbiór formuł
P
{ }
N
∪
nie jest spełniany, co w programowaniu w
logice sprowadza się do sprawdzenia, czy ze zbioru formuł
P
{ }
N
∪
można wyprowadzić
klauzulę pustą stosując
regułę rezolucji liniowej
(odpowiadającej stosowaniu bardziej
klasycznych: reguły odrywania i reguły podstawiania).
Jeżeli wykażemy, ze zbiór
P
{ }
N
∪
nie jest spełniany, to ze znanego faktu z logiki
otrzymujemy, że formuła
N
¬
wynika logicznie ze zbioru formuł tworzących program P.
Cel
N
ma postać:
m
B
B
,
,
1
K
←
,
czyli
(
)
Falsz
B
B
m
→
∧
∧
∀
K
1
.
Stąd na podstawie prawa KRZ:
(
)
p
Falsz
p
¬
→
→
mamy :
(
)
(
)
m
B
B
∧
∧
¬
∀
K
1
,
co jest równoważne
(
)
m
B
B
∧
∧
¬∃
K
1
.
Zatem formuła
(
)
m
k
B
B
x
x
∧
∧
∃
∃
K
K
1
1
wynika logicznie z
P
, gdzie
k
x
x
,
,
1
K
są zmiennymi
występującymi w
N
. Tym samym znajdziemy obiekty spełniające cel
N
.
REGUŁA REZOLUCJI ZDANIOWEJ
{
}
{
}
{
}
n
m
n
m
L
L
L
L
L
L
p
L
L
L
p
L
L
L
′
′
′
¬
′
′
′
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
2
1
2
1
2
1
2
1
K
K
K
K
,
n m
,
≥ 0
.
FAKT
Reguła rezolucji zdaniowej jest logiczną regułą wnioskowania, tzn. wniosek reguły rezolucji
zdaniowej wynika ze zbioru przesłanek tej reguły.
REZOLUCJA LINIOWA.
Niech P będzie programem definitywnym.
Reguła rezolucji liniowej
ma postać:
n
m
A
A
A
,
,
,
,
1
K
K
←
– cel
G
k
B
B
B
,
,
1
K
←
– wariant klauzuli
C
programu
P
____________________________________
(
)
σ
n
m
k
m
A
A
B
B
A
A
,
,
,
,
,
,
,
,
1
1
1
1
K
K
K
+
−
←
– nowy cel
gdzie
σ
jest MGU zbioru
{
}
A
B
m
,
, tzn.
A
B
m
σ
σ
=
.
Uzasadnienie:
G
:
(
)
n
m
A
A
A
∧
∧
∧
∧
¬
K
K
1
⇔
n
m
A
A
A
¬
∨
∨
¬
∨
∨
¬
K
K
1
C
:
k
B
B
B
¬
∨
∨
¬
∨
K
1
σ
:
B
A
m
σ
σ
=
Gσ
:
σ
σ
σ
n
m
A
A
A
¬
∨
∨
¬
∨
∨
¬
K
K
1
Cσ
:
σ
σ
σ
k
B
B
B
¬
∨
∨
¬
∨
K
1
___________________________________rezolucja zdaniowa_
σ
σ
σ
σ
σ
σ
n
m
k
m
A
A
B
B
A
A
¬
∨
∨
¬
∨
¬
∨
∨
¬
∨
¬
∨
∨
¬
+
−
K
K
K
1
1
1
1
c
(
)
σ
n
m
k
m
A
A
B
B
A
A
∧
∧
∧
∧
∧
∧
∧
∧
¬
+
−
K
K
K
1
1
1
1