Programowanie funkcyjne i programowanie w logice
__________________________________________________________________________________________
4. PROGRAMY DEFINITYWNE – podstawy programowania w Prologu.
WPROWADZENIE.
Klauzula : , gdzie – literał.
Literał : (pozytywny),
(negatywny), gdzie A – atom
.
Klauzula, czyli formuła postaci:
, gdzie – atomy
jest logicznie równoważna formule:
Na podstawie prawa KRZ: otrzymujemy:
co zapisujemy w postaci:
przy czym i .
W szczególności:
: , ponieważ pusta alternatywa jest zawsze fałszywa;
: , ponieważ pusta koniunkcja jest zawsze prawdziwa.
DEF. Klauzula definitywna.
Klauzulą definitywną nazywamy klauzulę zawierającą dokładnie jeden literał pozytywny ():
klauzula jednostkowa, fakt, która oznacza formułę , czyli zakładamy
prawdziwość A;
klauzula niejednostkowa, reguła; regułę w praktyce zapisujemy jako:
,
gdzie
A – head, głowa reguły,
– body, ciało reguły.
DEF. Program definitywny.
Programem definitywnym nazywamy dowolny skończony zbiór klauzul definitywnych, tzn. zbiór formuł postaci : .
Uwaga!
Język programu P musi zawierać przynajmniej jedną stałą. Jeżeli jej nie ma trzeba taką stałą dodać, aby tworzyć termy ustalone.
DEF. Klauzula celu.
Celem nazywamy klauzulę nie zawierającą literałów pozytywnych ():
która jest równoważna formule :
na podstawie tautologii KRZ: .
DEF. Klauzula Horna.
Klauzulą Horna nazywamy klauzulę zawierającą co najwyżej jeden literał pozytywny, tzn. klauzulę definitywną lub klauzulę celu.
DEF. Klauzula pusta.
Klauzulę pustą otrzymujemy w sytuacji : i oznaczamy: .
Klauzula pusta nie jest klauzulą Horna.
Klauzula pusta jest klauzulą zawsze fłszywą, ponieważ .
Klauzula Horna w postaci implikacyjnej występuje w trzech formach:
a) implikacji (reguły) : ,
b) stwierdzenia (faktu) : ,
c) celu (zapytania) : .
Strategia PROLOGu.
Niech P będzie programem definitywnym, a G – celem.
Bierzemy pod uwagę zbiór .
Jeżeli wykażemy, że zbiór nie jest spełnialny, to na podstawie FAKTU 2.2 otrzymamy, że formuła wynika logicznie ze zbioru formuł tworzących program P.
Cel G ma postać:
Zatem formuła
wynika logicznie z P, gdzie są wszystkimi zmiennymi występującymi w G.
Tym samym znajdziemy obiekty spełniające cel G.
REZOLUCJA LINIOWA.
Niech P będzie programem definitywnym.
DEF. Reguła rezolucji liniowej.
Reguła rezolucji liniowej ma postać:
– cel G
– wariant klauzuli C programu P
____________________________________
– nowy cel
gdzie jest MGU zbioru , tzn. .
Wniosek reguły rezolucji liniowej nazywamy rezolwentą liniową przesłanek.
Uzasadnienie:
G:
C:
:
___________________________________rezolucja zdaniowa_
DERYWACJA LINIOWA.
DEF. Derywacja liniowa.
Derywacja liniową dla nazywamy skończony lub nieskończony ciąg, którego wyrazami są
, lub
spelniający warunki:
a) dla każdego n, jest wariantem klauzuli programu P nie zawierającym zmiennych
występujących w ,
b) dla każdego n, jest rezolwentą liniową celu oraz klauzuli otrzymaną
za pomocą podstawienia .
DEF. Refutacja liniowa.
Liniową refutacją dla nazywamy skończoną liniową derywację dla , której ostatni cel jest klauzulą pustą.
DEF. Odpowiedź obliczona.
Niech będzie liniową refutacją dla . Odpowiedzią obliczoną dla wyznaczoną przez tę refutację nazywamy podstawienie ograniczone do zmiennych występujących w G, tzn. .
PRZYKŁAD 5.1
Wyznaczanie odpowiedzi obliczonej.
WYNIKANIE LOGICZNE W LPR
Przypomnienie:
DEF. Model zbioru formuł.
Interpretację M nazywamy modelem dla zbioru formuł , jeżeli wszystkie formuły ze zbioru są prawdziwe w M, co oznaczamy przez .
DEF. Wynikanie logiczne.
Formuła A wynika logicznie ze zbioru formuł , jeżeli formuła A jest prawdziwa we wszystkich modelach dla zbioru .
Wprowadzamy oznaczenie:
– formuła A wynika logicznie ze zbioru na gruncie LPR.
FAKT 5.1.
Wynikanie logiczne na gruncie LPR spełnia warunki konsekwencji, tzn.
(C1) jeżeli , to ,
(C2) jeżeli oraz , to ,
(C3) jeżeli dla wszystkich oraz , to .
FAKT 5.2.
Jeżeli jest dowolnym podstawieniem, a A – formułą LPR taką, że nie zachodzi kolizja zmiennych przy podstawieniu , to .
Dowód. Wynika z prawa LPR: .
WNIOSEK.
Jeżeli formuła A nie zawiera kwantyfikatorów (w szczególności, gdy A jest klauzulą), to dla każdego podstawienia : .
FAKT 5.3.
i .
Dowód FAKTu 5.3.
DEF. Odpowiedź poprawna.
Podstawienie nazywamy odpowiedzią poprawną dla , gdzie G: , jeżeli formuła wynika logicznie w LPR z programu P, co zapisujemy . Przyjmujemy dodatkowo, że dziedzina podstawienia ...
Wujek_Misiek