Programowanie funkcyjne i programowanie w logice.
__________________________________________________________________________________________
KLAUZULE
DEF. Literały.
Literałem pozytywnym nazywamy dowolną zmienną zdaniową , a literałem negatywnym negację zmiennej zdaniowej .
Literały oznaczamy: .
DEF. Klauzule.
Klauzulami nazywamy skończone zbiory literałów.
Klauzulę interpretujemy jako alternatywę .
Klauzule oznaczamy: ; klauzula pusta: ; - zbiór klauzul
DEF. Spełnianie klauzuli i zbioru klauzul przez wartościowanie.
1. Wartościowanie w spełnia klauzulę A (oznaczenie: ), jeżeli dla pewnego , .
2. Wartościowanie w spełnia zbiór klauzul (oznaczenie: ), jeżeli dla każdej klauzuli, .
DEF. Spełnialność klauzuli i zbioru klauzul.
1. Klauzulę A nazywamy spełnialną, jeżeli istnieje wartościowanie w takie, że .
2. Zbiór klauzul nazywamy spełnialnym, jeżeli istnieje wartościowanie w takie,
że .
DEF. Wynikanie klauzuli ze zbioru klauzul.
Klauzula A wynika ze zbioru klauzul w KRZ, jeżeli dla każdego wartościowania w zachodzi warunek: jeżeli , to .
FAKT 1.4.
Żadne wartościowanie nie spełnia klauzuli pustej .
Klauzule pusta interpretujemy jako stałą 0 (fałsz).
FAKT 1.5.
Następujące warunki są równoważne:
a) zbiór klauzulnie jest spełnialny,
b) klauzula pusta wynika ze zbioru klauzul .
Reguła rezolucji zdaniowej
, .
FAKT 1.6.
Reguła rezolucji zdaniowej jest logiczną regułą wnioskowania, tzn. wniosek reguły rezolucji zdaniowej wynika ze zbioru przesłanek tej reguły.
DEF. Rezolwenta.
Wniosek reguły rezolucji zdaniowej nazywamy rezolwentą jej przesłanek.
Weźmy pod uwagę zbiór , tzn. zbiór wszystkich skończonych ciągów o elementach 0, 1.
– ciąg pusty,
Przez xy będziemy oznaczać konkatenację (połączenie) ciągów x i y: x = 001, y = 100, xy = 001100.
DEF. Drzewo binarne.
Drzewem binarnym nazywamy skończony i niepusty zbiór spełniający warunki:
a) jeżeli , to ,
b) jeżeli ,to ; warunek ten mówi, że istnieją dwa lub zero potomków (następników).
Elementy zbioru X nazywamy wierzchołkami drzewa.
W szczególności:
nazywamy korzeniem drzewa X;
elementy , takie że i , to liście drzewa;
wierzchołki nazywamy bezpośrednimi potomkami wierzchołka .
PRZYKŁAD 1.5.
Drzewo binarne.
DEF. Drzewo etykietowane.
Etykietowanym drzewem binarnym nazywamy trójkę taką, że X jest drzewem binarnym, E jest niepustym zbiorem, a f – funkcją , . Elementy zbioru E nazywamy etykietami, jest etykietą wierzchołka x.
DEF. Derywacja klauzuli ze zbioru klauzul.
Derywacją klauzuli A ze zbioru klauzul nazywamy drzewo etykietowane takie, że:
1) E jest zbiorem klauzul ;
2) dla każdego liścia x drzewa X, ;
3) ;
4) dla każdego wierzchołka x drzewa X nie będącego liściem jest rezolwentą
etykiet bezpośrednich potomków wierzchołka x.
DEF. Wyprowadzalność klauzuli ze zbioru klauzul przez rezolucję zdaniową : .
Klauzula A jest wyprowadzalna ze zbioru klauzul przez rezolucję zdaniową, jeżeli istnieje derywacja klauzuli A ze zbioru .
PRZYKŁAD 1.6.
Derywacja klauzuli ze zbioru klauzul.
DEF. Refutacja zbioru klauzul.
Derywację klauzuli pustej ze zbioru klauzul nazywamy refutacją zbioru .
PRZYKŁAD 1.7.
Refutacja zbioru klauzul.
TWIERDZENIE 1.1. O poprawności (zgodności) rezolucji zdaniowej.
Jeżeli , to A wynika ze zbioru .
Dowód TW 1.1
TWIERDZENIE 1.2. O pełności rezolucji zdaniowej.
Jeżeli klauzula pusta wynika ze zbioru klauzul , to .
TWIERDZENIE 1.3. O zgodności i pełności rezolucji zdaniowej.
Następujące warunki są równoważne.
1) zbiór nie jest spełnialny,
2) .
Dowód TW 1.3.
FAKT 1.7.
Jeżeli zbiór jest skończony, to istnieje algorytm sprawdzania czy .
ZASTOSOWANIE REZOLUCJI ZDANIOWEJ DO SPRAWDZANIA TAUTOLOGICZNOŚCI FORMUŁ KRZ
DEF. Koniunkcyjna postać normalna.
Formuła KRZ jest w koniunkcyjnej postaci normalnej, jeżeli jest koniunkcją alternatyw literałów, tzn. ma postać:
Algorytm 1.1. Sprowadzanie formuł KRZ do koniunkcyjnej postaci normalnej KPN.
Dane : formuła A
Wynik : formuła KPN(A) równoważna formule A i będąca w postaci KPN
(1) przyjmujemy początkowo, że formuła B jest identyczna z formułą A
(2) eliminujemy z B niechciane spójniki i zastępując odpowiednio:
przez
(3) wprowadzamy znak negacji do wnętrza oraz usuwamy
podwójną negację zastępując odpowiednio:
przez C
(4) stosujemy rozdzielczość koniunkcji względem alternatywy
zastępując odpowiednio:
(5) formułę KPN(A) definujemy teraz jako formułę B.
DEF. Postać klauzulowa formuły w KPN.
Postacią klauzulową formuły A w KPN
nazywamy zbiór klauzul :
FAKT 1.8.
Nastepujące warunki są równoważne
(i)
(ii)
(iii)
Algorytm 1.2. Sprawdzanie tautologiczności formuł KRZ za pomocą rezolucji zdaniowej.
Wynik : odpowiedź tak, jeżeli formuła A jest tautologia KRZ, odpowiedź nie w przeciwnym przypadku
(1) bierzemy formułę B identyczną z formułą .
(2) sprowadzamy formułę B do koniunkcyjnej postaci normalnej KPN(B)
(3) formułę KPN(B) przedstawiamy w postaci klauzulowej
(4) szukamy derywacji klauzuli pustej ze zbioru
(5) jeżeli klauzula pusta została otrzymana, odpowiedź tak
(6) jeżeli algorytm zatrzymał się ze względu na brak możliwości stosowania reguły rezolucji,
odpowiedź nie.
Maria Bulińska 12
Wujek_Misiek