Transcript
1. Metoda tabel semantycznych Udowodnić prawdziwość formuły metodą tabel semantycznych: (A→B) →(¬B→¬A) ZALECAMY podkreślanie analizowanych formuł, W celu zbadania prawdziwości formuły należy zanegować formułę i udowodnić niespełnialność negacji. ¬ [(A→B) →(¬B→¬A)]
(A→B), ¬ (¬B→¬A)
(A→B), ¬B, ¬¬A
(A→B), ¬B, A
¬A, ¬ B, A
B , ¬ B, A
× × ODP.: Ponieważ wszystkie liście drzewa są domknięte, zatem drzewo jest domknięte, co oznacza że zanegowana formuła jest niespełnialna (sprzeczna). Stąd formuła oryginalna jest prawdziwa.
2. Udowodnić prawdziwość formuły metodą tabel semantycznych: (((A→B) →A)→A) W celu zbadania prawdziwości formuły należy zanegować formułę i udowodnić niespełnialność negacji. ¬ [((A→B) →A)→A]
((A→B) →A), ¬A
¬(A→B), ¬A
A, ¬B, ¬A
A, ¬A ×
× ODP.: Ponieważ wszystkie liście drzewa są domknięte, zatem drzewo jest domknięte, co oznacza że zanegowana formuła jest niespełnialna (sprzeczna). Stąd formuła oryginalna jest prawdziwa.
3. Zbadać spełnialność formuły metodą tabel semantycznych: (((A→B) →B)→A) ((A→B) →B)→A
¬ ((A→B) →B)
A •
(A→B), ¬ B
¬A, ¬ B •
B, ¬ B ×
ODP.: Ponieważ istnieją liście otwarte, zatem formuła jest spełnialna. Z liści otwartych można odczytać modele. Z liścia (¬A, ¬ B) odczytamy model: v(A) = 0 i v(B) = 0. Z liścia (A) odczytamy modele: v(A) = 1 i v(B) dowolne (0 lub 1). Liście te nie mają modeli wspólnych, zatem wszystkich modeli formuły mamy 3.
Komentarz do Metody Tabel Semantycznych Metoda tabel semantycznych poszukuje modelu (modeli) formuły. Modele te można odczytać z liści otwartych (przypominam, że są dwa rodzaje liści i model można odczytać tylko z jednego rodzaju liści). Jeżeli dany liść pozwala na odczytanie modelu formuły, to można odczytać z tego liścia dokładnie jeden model lub więcej. Liczba modeli, które można odczytać z takiego liścia zależy od postaci zbioru literałów tworzących liść (zbiór literałów w liściu traktujemy jako koniunkcję tych literałów). Wystąpienie literału w liściu definiuje bowiem wartościowanie odpowiedniego atomu, tworzącego ten literał. Przypominamy, że Metoda tabel semantycznych nie daje odpowiedzi wprost na pytanie: czy formuła jest prawdziwa. Zatem drzewo, które posiada wyłącznie liście otwarte, nie jest dowodem na to, że formuła jest prawdziwa – można to pokazać na przykładzie formuły: p lub q Można też zadać pytanie (dodatkowe) czy Metoda tabel semantycznych pokazuje wszystkie możliwe modele?
2. DBD 1. Niech A = ((p∧q) ∨ r). Sprawdź czy formuła ∃p A jest spełniona 1) zbudować DBD dla rozważanej formuły A, 2) w oparciu o ten diagram zbudować DWA diagramy (dla formuły A|p=0 i A|p=1), 3) oraz zastosować algorytm łączenia drzew. Jeżeli kwantyfikator jest typu ∃ łączymy te dwa diagramy operatorem ∨, jeżeli zaś kwantyfikator jest typu ∀ łączymy te dwa diagramy operatorem ∧. 2a. ((p∧q) ∨ r) |p=0
1. ((p∧q) ∨ r) r
r
r
1
p
p
R 0
q
q
0
1
0
0
1
3. ((p∧q) ∨ r) |p=0 ∨ ((p∧q) ∨ r) |p=1 (kolejność zmiennych: rq)
2b. ((p∧q) ∨ r) |p=1
r
r
q
0
r
1
q
0
1
1
R
q
0
1
1
„R” oznacza REDUKCJĘ
ODP.: Ponieważ w wynikowym diagramie znajduje się węzeł o wartości „1” zatem formuła ∃p A jest spełniona (formuła A jest spełniona dla pewnej wartości atomu p).
2. Niech A = ((q∧p) ∨ r). Sprawdź czy formuła ∀p A jest spełniona 1) zbudować DBD dla rozważanej formuły A, 2) w oparciu o ten diagram zbudować DWA diagramy (dla formuły A|p=0 i A|p=1), 3) oraz zastosować algorytm łączenia drzew. Jeżeli kwantyfikator jest typu ∃ łączymy te dwa diagramy operatorem ∨, jeżeli zaś kwantyfikator jest typu ∀ łączymy te dwa diagramy operatorem ∧.
1. ((q∧p) ∨ r)
2a. ((q∧p) ∨ r) |p=0
r
r
r
r
R 1
q
q
0
q
1
R 0
p
p
0
1
0
1
2b. ((q∧p) ∨ r) |p=1
0
1
3. ((q∧p) ∨ r) |p=0 ∧ ((q∧p) ∨ r) |p=1 (kolejność zmiennych: rq)
r r q 0
0
1
1
„R” oznacza REDUKCJĘ
ODP.: Ponieważ w wynikowym diagramie znajduje się węzeł o wartości „1” zatem formuła formuła ∀p A jest spełniona (formuła A jest spełniona dla każdej wartości atomu p).
Komentarz do Diagramów Binarnych Decyzji Diagramy Binarnych Decyzji, w odróżnieniu od większości metod, pozwalają na badanie wprost nie tylko spełnialności ale także prawdziwości. Formuła prawdziwa, przypominam, ma w każdej interpretacji wartość reprezentowaną przez symbol 1, co jest wyraźnie widoczne w zredukowanym diagramie binarnych decyzji. Istnieje twierdzenie mówiące, że zredukowane diagramy UDBD dla formuł logicznie równoważnych są strukturalnie identyczne dla poszczególnych uporządkowań atomów. Podkreślmy: dla poszczególnych uporządkowań atomów. Kwantyfikacja jest pytaniem o spełnialność formuły dla pewnej lub wszystkich wartości kwantyfikowanego atomu. Istnieje możliwość zastosowania kilku kwantyfikatorów do formuły, ale oznacza to, że należy zachować odpowiedni porządek analizowania tych kwantyfikatorów. Wprawdzie w materiałach nie ma o tym wprost mowy, ale żeby dokonać analizy dowolnego kwantyfikatora, należy najpierw poddać analizie kwantyfikatory umieszczone na prawo (najbardziej zagnieżdżone).
3. Rachunek predykatów - semantyka Rozważmy problem badania spełnialności/ niespełnialności oraz prawdziwości/nieprawdziwości. Rozpocznijmy od INTERPRETACJI, która jest bardziej złożona niż w rachunku zdań. Musimy bowiem podać: dziedzinę interpretacji, relację, funkcję, oraz wartość stałej. Wartościowanie to funkcja ̙σI: V -> D W wartościowaniu możemy podać dokładną wartość podstawioną zmiennej: σI [x<-d] Wartość termu t w interpretacji I i wartościowaniu σI to vσI(t) Wartość formuły A w interpretacji I przy wartościowaniu σI to vσI(A) i definiujemy przez indukcję ze względu na budowę formuły (kwantyfikatory, operatory, symbole funkcyjne) TW. Niech A będzie formułą zamkniętą. Wówczas vσI(A) NIE ZALEŻY od wartościowania σI. Zadanie: zbadaj spełnialność / prawdziwość formuły A = ∃y∀x p(x,y) 1. 2. 3. 4. 5.
Podajemy interpretację: I = {N, {>=}, {}, {}} Formuła w interpretacji: ∃y ∈N ∀x∈N x>=y Wartość formuły przy wartościowaniu: vσI[y<-0, x<-d](p(x,y))=1 dla każdego d ∈N Wartość formuły zamkniętej (korzystamy z Twierdzenia) : vσI(∃y∀x p(x,y)) =1 I |= A
Wniosek – formuła jest spełnialna ponieważ istnieje interpretacja, w której vσI(∃y∀x p(x,y)) = 1 A czy formuła jest nieprawdziwa? 6. 7. 8. 9.
Podajemy interpretację: I = {{5}, {≠}, {}, {}} Formuła w interpretacji: ∃y ∈{5} ∀x∈{5} x≠y Wartość formuły przy wartościowaniu: vσI[y<-5, x<-d](p(x,y))=0 dla każdego d ∈{5} Wartość formuły zamkniętej (korzystamy z Twierdzenia) : vσI(∃y∀x p(x,y)) =0
10. Wniosek – formuła jest nieprawdziwa, ponieważ istnieje interpretacja, w której vσI(∃y∀x p(x,y)) = 0
4. Modele Herbranda Rozszerzenie zbioru termów przez wprowadzenie symboli funkcyjnych powoduje, że zbiór możliwych interpretacji staje się złożony (przeliczalnie nieskończony). Jest zadaniem trudnym (a nawet niemożliwym) rozważać wszystkie interpretacje dla wszystkich dziedzin żeby wykazać, że formuła jest niespełnialna. Rozwiązaniem byłoby rozważanie pewnej stałej dziedziny H, takiej że zbiór klauzul S odpowiadający danej formule jest niespełnialny we wszystkich interpretacjach dla tej dziedziny H. Taką dziedziną jest uniwersum Herbranda HS. Definicja: Niech S będzie zbiorem klauzul. Uniwersum Herbranda HS jest zbiorem wszystkich termów ustalonych utworzonych z symboli występujących w S. Jeśli w S nie występuje stała, HS jest inicjowane wprowadzeniem dowolnej stałej a Definicja: Termem (atomem, formułą) ustalonym nazywamy term (atom, formułę), który nie zawiera zmiennych. Przykład: Dany jest zbiór klauzul S = {p(x) ∨ q(x), r(f(y))} HS = {a, f(a), f(f(a)), f(f(f(a)), f(f(f(f(a))), f(f(f(f(f(a)))), …} Definicja: Niech HS będzie uniwersum Herbranda zbioru klauzul S. Bazą Herbranda BS nazywamy zbiór atomów ustalonych utworzonych z symboli predykatywnych występujących w S oraz termów należących do HS. Baza Herbranda jest także nazywana zbiorem atomów. Przykład cd. BS = {p(a), q(a), r(a), p(f(a)), q(f(a)), r(f(a)), p(f(f(f(a)))), q(f(f(f(a)))), r(f(f(f(a)))), …} Definicja: Interpretacją Herbranda dla zbioru klauzul S nazywamy interpretację, której dziedziną jest uniwersum Herbranda zbioru S, a stałym i symbolom funkcyjnym są przyporządkowane te same symbole: v(a) = a, v(f(t1,…tn)) = f(v(t1),…, v(tn)). Nie nakłada się ograniczeń na przyporządkowanie symbolom predykatywnym relacji określonych nad uniwersum Herbranda. Niech BS = {A1,A2, … } będzie bazą Herbranda. Interpretacja Herbranda może być przedstawiona jako zbiór {m1,m2,…} gdzie mj jest albo Aj albo ~Aj. Przykład cd. I1 = {p(a), q(a), r(a), p(f(a)), q(f(a)), r(f(a)), p(f(f(f(a)))), q(f(f(f(a)))), r(f(f(f(a)))), …} I2 = {~p(a), q(a), r(a), p(f(a)), q(f(a)), r(f(a)), p(f(f(f(a)))), q(f(f(f(a)))), r(f(f(f(a)))), …} I3 = {p(a), ~q(a), r(a), p(f(a)), q(f(a)), r(f(a)), p(f(f(f(a)))), q(f(f(f(a)))), r(f(f(f(a)))), …} I3 = {~p(a), ~q(a), r(a), p(f(a)), q(f(a)), r(f(a)), p(f(f(f(a)))), q(f(f(f(a)))), r(f(f(f(a)))), …} Definicja: Modelem Herbranda zbioru klauzul S nazywamy interpretację Herbranda spełniającą S. Model Herbranda można utożsamić z podzbiorem bazy Herbranda, zawierającym atomy, dla których v(p(t1,…,tn)) = 1.
5. Podstawienia Zastosowanie podstawienia do wyrażenia ZADANIE: E = p(x) ∨ q(y) θ = {x ← y, y ← f(a)}
oblicz Eθ
Odp. Eθ = p(y) ∨ q(f(a)) Składanie podstawień ZADANIE: złóż podstawienia θ = {x ← f(y), y ← f(a), z ← u} δ = {y ← g(a), u ← z, v ← f(f(a))} Odp. θδ = { x ← f(g(a)), y ← f(a)} u {u ← z, v ← f(f(a))}
6. Uzgadnianie ZADANIE: Znajdź „mgu” dla wyrażeń: A = p( g(y) , f(x,h(x),y) ) oraz A’ = p( x , f(g(z),w,z) ) Są 4 reguły postepowania (wybór reguł dowolny) g(y) = x f(x,h(x),y) = f(g(z),w,z)
zamiana stron zastąpienie równania równaniami dla każdej pary argumentów
x = g(y) x = g(z) h(x) = w y=z
użycie termu g(y) w innych równaniach, gdzie wystąpi x
x = g(y) g(y) = g(z) h(g(y)) = w y=z x = g(z) g(z) = g(z) h(g(z)) = w y=z
użycie termu z w innych równaniach, gdzie występuje y
usuwamy równanie, w którym obie strony są identyczne zamiana stron
x = g(z) w = h(g(z)) y=z Odp. „mgu” to
{x← g(z), w← h(g(z)), y← z }
7. Skolemizacja 1. Sprowadzić do postaci klauzulowej: ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) (Zakładamy, że wszystkie wystąpienia zmiennych są związane !!!) Dla przypomnienia zasięg kwantyfikatorów: ∃z : ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) ∀u : ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) ∀u: ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧ ∀y∃v q(y,v) ) ) ∃r : ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) ∀y: ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) ∃v : ∃z ( ∀u p(z,u) → ∀u (∃r q(r,u) ∧∀y∃v q(y,v) ) ) Krok 1: przemianowanie zmiennych ∃z ( ∀u p(z,u) → ∀s (∃r q(r,s) ∧∀y∃v q(y,v) ) ) Krok 2: zmiana operatorów ∃z (¬∀u p(z,u) ∨ ∀s (∃r q(r,s) ∧ ∀y∃v q(y,v) ) ) Krok 3: przesunięcie negacji ∃z (∃u ¬p(z,u) ∨ ∀s (∃r q(r,s) ∧ ∀y∃v q(y,v) ) ) Krok 4: wydobycie kwantyfikatorów: ∃z (∃u ¬p(z,u) ∨ ∀s (∃r q(r,s) ∧ ∀y∃v q(y,v) ) ) ∃z ∃u (¬p(z,u) ∨ ∀s (∃r q(r,s) ∧ ∀y∃v q(y,v) ) ) ∃z ∃u (¬p(z,u) ∨ ∀s ∃r (q(r,s) ∧ ∀y∃v q(y,v) ) ) ∃z ∃u∀s (¬p(z,u) ∨ ∃r (q(r,s) ∧ ∀y∃v q(y,v) ) ) ∃z ∃u∀s ∃r (¬p(z,u) ∨ (q(r,s) ∧ ∀y∃v q(y,v) ) ) ∃z ∃u∀s ∃r (¬p(z,u) ∨ ∀y (q(r,s) ∧ ∃v q(y,v) ) ) ∃z ∃u∀s ∃r ∀y (¬p(z,u) ∨ (q(r,s) ∧ ∃v q(y,v) ) ) ∃z ∃u∀s ∃r ∀y (¬p(z,u) ∨ ∃v (q(r,s) ∧ q(y,v) ) ) ∃z ∃u∀s ∃r ∀y ∃v (¬p(z,u) ∨ (q(r,s) ∧ q(y,v) ) )
możemy ∃u, ∀s, ∃r, ∀y, nie możemy ∃v możemy ∀s, ∃r, ∀y, nie możemy ∃v możemy ∀s, ∀y, nie możemy ∃r , ∃v możemy ∃r, ∀y, nie możemy ∃v możemy ∀y, nie możemy ∃v możemy ∀y, ∃v możemy ∃v możemy ∃v
Krok 5: koniunkcyjna postać normalna ∃z ∃u∀s ∃r ∀y ∃v ( (¬p(z,u) ∨ q(r,s)) ∧ (¬p(z,u) ∨ q(y,v)) ) Krok 6: Funkcja Skolema - ∃u∀s ∃r ∀y ∃v ( (¬p(a,u) ∨ q(r,s)) ∧ (¬p(a,u) ∨ q(y,v)) ) - - ∀s ∃r ∀y ∃v ( (¬p(a,b) ∨ q(r,s)) ∧ (¬p(a,b) ∨ q(y,v)) ) - - ∀s - ∀y ∃v ( (¬p(a,b) ∨ q(f1(s),s)) ∧ (¬p(a,b) ∨ q(y,v)) ) - - ∀s - ∀y - ( (¬p(a,b) ∨ q(f1(s),s)) ∧ (¬p(a,b) ∨ q(y, f2(s,y))) ) Powyższą formuła jest w postaci klauzulowej, ale można ją przedstawić także jako zbiór klauzul, pomijając kwantyfikatory (gdyż wszystkie zmienne są kwantyfikowane uniwersalnie): {
{¬p(a,b) , q(f1(s),s)} , {¬p(a,b) , q(y, f2(s,y)) } }
Komentarz do Skolemizacji Skolemizacja przekształca formułę do postaci klauzulowej. Postać normalna dopuszcza bowiem kwantyfikatory egzystencjalne. Jednakże my jesteśmy zainteresowani wyłącznie kwantyfikatorami uniwersalnymi, stąd ostatni krok skolemizacji, przekształcający postać normalną do klauzulowej. Postać klauzulową można zapisać w postaci zbioru klauzul. Skolemizacja, do przedostatniego kroku zachowuje logiczną równoważność. Zastosowanie funkcji Skolema nie zachowuje już logicznej równoważności, lecz spełnialność. W większości przypadków badamy jednak spełnialność formuł, stąd Skolemizacja jest użyteczna. Tw. Formuła uzyskana na drodze Skolemizacji jest niespełniana wtw, gdy wyjściowa formuła jest niespełnialna
Skolemizacja wymaga formuły zamkniętej. Formuła jest zamknięta, jeżeli nie ma zmiennych wolnych. Zmienna jest wolna, jeżeli chociaż jedno jej wystąpienie jest wolne. Zmienna jest związana, jeżeli wszystkie jej wystąpienia są związane. Wystąpienie zmiennej jest związane wtw, gdy znajduje się w zakresie odpowiedniego kwantyfikatora. Wystąpienie zmiennej jest wolne wtw, gdy nie jest związane.
8. Rezolucja w rachunku predykatów a) Udowodnij za pomocą metody rezolucji, że następujący zbiór klauzul jest niespełniany; C1: ¬p(x1) ∨ ¬r(x1) ∨ s(x1) C2: q(b) C3: ¬q(b) ∨ r(x3) C4: p(a) C5: ¬s(x5) Rezolwenta dla C5 i C1 to C6: ¬p(x5) ∨ ¬r(x5) Rezolwenta dla C6 i C4 to C7: ¬r(a) Rezolwenta dla C7 i C3 to C8: ¬q(b) Rezolwenta dla C8 i C2 to C9:
podstawienie uzgadniające s1: {x1 <- x5} podstawienie uzgadniające s2: {x5 <- a} podstawienie uzgadniające s3: {x3 <- a} podstawienie uzgadniające s4: {}
ODP. Zbiór klauzul jest niespełniany
b) Podaj najbardziej ogólne podstawienie uzgadniające („mgu”) z uzyskanych podstawień ODP. MGU (złączenie wszystkich podstawień czyli: s1s2s3s4) = {x1<-a, x5<-a, x3<-a}
Komentarz do Rezolucji Zauważmy, że C5 to zanegowany cel, który jest badany i na początku jest on łączony z dowolną inną klauzulą. Następnie dla uzyskanej rezolwenty szukamy klauzuli z oryginalnego zbioru klauzul. Jest to proponowana strategia poszukiwanie klauzuli pustej. MGU pozwala odczytać, dla jakiej wartości zmiennej nasz cel jest konsekwencją logiczną zbioru klauzul – trzeba jedynie znaleźć odpowiednie podstawienie, będące elementem mgu.
1) Jaś na wycieczce w ZOO zobaczył pingwina. Po powrocie do domu zaczął zastanawiać się, czy pingwin jest ptakiem czy ssakiem. Pamiętał, że pingwin z ZOO miał dziób i skrzydła. Niestety Jaś nie pamiętał, czy pingwin miał pióra (a tylko ptaki mają pióra). Natomiast Jaś z lekcji biologii pamiętał, że dzioby mają nie tylko ptaki ale też ssak dziobak. Ponadto przypomniał sobie, że skrzydła mają nie tylko ptaki ale też ssak nietoperz. Zapisał to w postaci reguł: ∀x [ma(x,dziób) -> (ptak(x) ∨ ssak(x))] ∀y [ma(y,skrzydła) -> (ptak(y) ∨ ssak(y))] Jaś nie przypominał sobie, żeby istniał ssak, który miałby jednocześnie dziób i skrzydła, zatem zapisał: ∀z [ssak(z) -> ¬ (ma(z,dziób) ∧ ma(z,skrzydła))] Jaś zapisał fakty, przekształcił reguły do postaci klauzulowej i otrzymał zbiór (koniunkcja) klauzul U: C1: ma(pingwin, dziób) C2: ma(pingwin, skrzydła) C3: ¬ ma(x,dziób) ∨ ptak(x) ∨ ssak(x) C4: ¬ ma(y,skrzydła) ∨ ptak(y) ∨ ssak(y) C5: ¬ssak(z) ∨ ¬ma(z,dziób) ∨ ¬ma(z,skrzydła) 2) Sprawdź, za pomocą metody rezolucji, czy formuła ptak(pingwin) jest logiczną konsekwencją w.w zbioru klauzul U (2p.) Czy formuła ptak(pingwin) jest logiczną konsekwencją pustego zbioru klauzul? Uzasadnij odpowiedź Rozwiązanie: formuła A jest logiczną konsekwencją zbioru U wtw, gdy U -> A jest formułą prawdziwą. Będziemy badać prawdziwość nie wprost – badamy niespełnialność formuły: ¬ (U -> A) która jest logicznie równoważna formule U ∧ ¬A. Dodajemy zatem do zbioru U klauzulę C6: ¬ptak(pingwin) i stosujemy metodę rezolucji Rezolwenta C6 i C3 to C7: ¬ ma(pingwin,dziób) ∨ ssak(pingwin) Rezolwenta C7 i C1 to C8: ssak(pingwin) Rezolwenta C8 i C5 to C9: ¬ma(pingwin,dziób) ∨ ¬ma(pingwin,skrzydła) Rezolwenta C9 i C1 to C10: ¬ma(pingwin,skrzydła) Rezolwenta C10 i C2 to C11:
podst.(x<- pingwin) podst.(z<- pingwin)
Odp. 1. Ponieważ U ∧ ¬A i zarazem ¬ (U -> A) jest niespełniana, zatem (U -> A) jest prawdziwa co jest dowodem na to że formuła ptak(pingwin) jest logiczną konsekwencją zbioru U
Odp. 2 formuła A jest logiczną konsekwencją zbioru U wtw gdy U -> A jest formułą prawdziwą. W naszym wypadku U jest pustym zbiorem klauzul, czyli jest formułą prawdziwą. Zatem, żeby formuła (U -> A) była prawdziwa, formuła A musi być prawdziwa. Formuła A jest formułą zamkniętą. Możemy podać interpretację w której predykat ptak(x) reprezentuje relację, że x jest ptakiem a stała pingwin reprezentuje zwierze pingwin. W tej interpretacji formuła A jest spełniona, ale można podać inne interpretacje, w których formuła A nie będzie spełniona (np. stała pingwin reprezentuje osobę, która wygrała w ping-ponga). Zatem A nie jest prawdziwa i nie jest logiczną konsekwencją pustego zbioru klauzul.
9. Równoważność logiczna W logice formuły mają więcej niż jedną wartość logiczną. Stąd porównywanie formuł nie może być oparte o relację równości. Wprowadzona została relacja równoważności logicznej. Istnieje definicja równoważności logicznej oraz Twierdzenie, które jest stosowane w badaniu formuł: Tw. A1≡ A2 wtw, gdy formuła A1↔A2 jest prawdziwa.
10. Konsekwencja logiczna Definicja konsekwencji logicznej: Niech U będzie zbiorem formuł, A zaś formułą. Jeżeli w każdym modelu U wartością A jest 1, to A nazywamy konsekwencją logiczną U, co zapisujemy U |=A Jeżeli zbiór U jest pusty, to pojęcie konsekwencji logicznej jest tożsame z pojęciem prawdziwości. Zauważmy, że formuła A może mieć więcej modeli niż U (formuła A może mieć modele, które nie są modelami dla U). Ale, te modele, które są modelami dla U muszą być także modelami dla A Przypominamy, że zbiór formuł U ma model , jeżeli istnieje interpretacja taka, że model ten jest modelem każdego elementu zbioru U. Zatem możemy sprowadzić poszukiwanie modelu dla zbioru U do poszukiwania modelu dla formuły będącej koniunkcją formuł tworzących U. Istnieje ponadto twierdzenie, które pozwala badać konsekwencję logiczną: Tw. U |=A wtw, gdy |=U →A (gdzie U to koniunkcja formuł tworzących U), czyli gdy U →A jest tautologią Badanie czy |=U →A (badanie prawdziwości formuły U →A) realizowane jest nie wprost – badamy niespełnialność formuły: ¬ (U -> A) która jest logicznie równoważna formule U ∧ ¬A. Konsekwencja logiczna jest czasami nazywana implikacją logiczną
