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=(RelL;FunL;ConL;�L)
taki, że
 Re lL jest niepustym zbiorem (symboli relacyjnych),
 FunL jest zbiorem (symboli funkcyjnych),
 ConL jest zbiorem (stałych przedmiotowych),
przy czym zbiory Re lL , FunL i ConL 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 ,
 f(t1,& ,tn) jest termem, jeżeli f"FunL , �L f =n oraz t1,& ,tn są tremami.
( )
Formułami atomowymi języka L nazywamy wyrażenia
R(t1,& ,tn),
takie że R"Re lL , �L R =n a t1,& ,tn 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 "(L1("L2("& ("Ln), gdzie Li , i=1,2,& , n są literałami.
Przykład klauzuli: "x"y(P(x, y)("Q(f(x),(y), a))
h
Klauzula postaci:
"(A1 ("& (" Ak (" ŹB1 ("& (" ŹBm)
jest równoważna formule
"((A1("& ("Ak)("Ź(B1'"& '"Bm)),
która z kolei jest równoważna formule
"(B1'"& '"BmA1("& ("Ak).
Formułę tę zapisujemy w postaci:
A1 ,
14,& ,3k�!11,& ,4Bm
24A B423
wniosek przeslanka
przecinki w przesłance (poprzednik implikacji) oznaczają koniunkcje,
przecinki we wniosku (następnik implikacji) oznaczają alternatywy.
Przykład:
klauzula: "x"y(P(x)("ŹA("ŹQ(y)("B)
zapis: P(x), B�!A,Q(y)
Szczególne przypadki klauzul:
k=1
Wtedy klauzula jest postaci:
A�!B1,& , Bm
Klauzulę tej postaci nazywamy klauzula definitywną.
W szczególności m=0 .
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ą.
k=0, m>0 .
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�!B1,& , Bm
Klauzulę taką nazywamy negatywną.
k=0, m=0 .
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:
A�!B1,& , Bm , ne"0
nagłówek treść, ciało
tzn. klauzul definitywnych (reguł) ( n>0 ) i klauzul jednostkowych, czyli faktów ( n=0 ).
Nieformalne znaczenie klauzuli definitywnej: dla każdego wartościowania zmiennych,
jeżeli Bi , i=1,2,& , m 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:
A�!B1,& , Bm , ne"0
a) deklaratywna (opisowa): A jest prawdziwe, jeśli B1,& , Bm są prawdziwe,
b) proceduralna (operacyjna): aby rozwiązać A rozwiąż B1,& , Bm .
Definicją predykatu (relacji, związku, własności) P / n (predykat P o n argumentach) w
programie w języku logiki P nazywamy zbiór wszystkich klauzul, w których nagłówku
występuje P / n .
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 LP .
Zadanie do rozwiązania przedstawione jest w postaci tzw. celu (ang. goal), zapytania.
Zapytanie jest to klauzula negatywna N, taka że N"LP .
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ć:
�!B1,& , Bm ,
czyli
"(B1 '"& '" Bm Falsz).
Stąd na podstawie prawa KRZ: (p Falsz) Źp mamy :
"(Ź(B1'"& '"Bm)) ,
co jest równoważne
Ź"(B1'"& '"Bm).
Zatem formuła "x1& "xk(B1'"& '"Bm) wynika logicznie z P, gdzie x1,& , xk są zmiennymi
występującymi w N. Tym samym znajdziemy obiekty spełniające cel N.
REGUA
A REZOLUCJI ZDANIOWEJ
{L1, L2& , Lm , p}
,
2 2 2
{L1, L2& , Ln ,Źp}
,
2 2 2
{L1, L2& , Lm , L1, L2& , Ln}, n, me"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ć:
�!A1,& , Am& , An  cel G
,
B�!B1,& , Bk  wariant klauzuli C programu P
____________________________________
�!(A1,& , Am-1, B1,& , Bk , Am+1,& , An)�  nowy cel
gdzie � jest MGU zbioru Am , B , tzn. Am�=B�.
{ }
Uzasadnienie:
G: Ź(A1'"& '"Am'"& '"An) �! ŹA1 ("& (" ŹAm ("& (" ŹAn
C: B (" ŹB1 ("& (" ŹBk
�: B�=Am�
G�: ŹA1�("& (" ŹAm�("& (" ŹAn�
C�: B�("ŹB1�("& ("ŹBk�
___________________________________rezolucja zdaniowa_
ŹA1�("& (" ŹAm-1�(" ŹB1�("& (" ŹBk�(" ŹAm+1�("& (" ŹAn�
c
Ź(A1'"& '"Am-1'"B1'"& '"Bk'"Am+1'"& '"An)�