Do tej pory pokazaliśmy, jak wyznaczać wnioskowanie przez sprawdzanie modeli: wyliczając modele i pokazując, że zdanie musi obowiązywać we wszystkich modelach. W tym podrozdziale pokazujemy, w jaki sposób można przeprowadzić wywodzenie przez dowodzenie twierdzeń – zastosowanie reguł wnioskowania bezpośrednio do zdań w naszej bazie wiedzy w celu skonstruowania dowodu pożądanego zdania bez konsultacji z modelami. Jeśli liczba modeli jest duża, ale długość dowodu jest krótka, to dowodzenie twierdzenia może być bardziej efektywne niż sprawdzanie modelu. Zanim zagłębimy się w szczegóły algorytmów dowodzenia twierdzeń, będziemy potrzebować kilku dodatkowych pojęć związanych z wnioskowaniem. Pierwsza koncepcja to równoważność logiczna: dwa zdania α i β są logicznie równoważne, jeśli są prawdziwe w tym samym zbiorze modeli. Zapiszemy to jako α ≡ β (Zauważ, że ≡ służy do wyrażania twierdzeń o zdaniach, podczas gdy jest używane jako część zdania.) Na przykład możemy łatwo pokazać (używając tabel prawdy), że P Λ Q i Q Λ P są logicznie równoważne. Te równoważności odgrywają w logice tę samą rolę, co tożsamości arytmetyczne w zwykłej matematyce. Alternatywna definicja równoważności jest następująca: dowolne dwa zdania α i β są równoważne wtedy i tylko wtedy, gdy każde z nich pociąga za sobą drugie:
α ≡ β jeśli i tylko jeśli α |= β i β |= α
Drugim pojęciem, którego będziemy potrzebować, jest zasadność. Zdanie jest ważne, jeśli jest prawdziwe we wszystkich modelach. Na przykład ważne jest zdanie P V ¬P. Prawidłowe zdania są również znane jako tautologie – są z konieczności prawdziwe. Ponieważ zdanie Prawda jest prawdziwe we wszystkich modelach, każde poprawne zdanie jest logicznie równoważne z Prawdą. Jakie są dobre zdania? Z naszej definicji implikacji możemy wyprowadzić twierdzenie o dedukcji, które było znane starożytnym Grekom:
Dla dowolnych zdań α i β, (α |- β) wtedy i tylko wtedy, gdy zdanie (α ⇒ β) zdanie jest ważne.
Ostatnią koncepcją, której będziemy potrzebować, jest satysfakcja. Zdanie jest spełnialne, jeśli jest prawdziwe w jakimś modelu lub jest przez niego spełnione. Na przykład podana wcześniej baza wiedzy (R1 Λ R2 Λ R3 Λ R4 Λ R5) jest zadowalająca, ponieważ istnieją trzy modele, w których jest ona prawdziwa. Spełnialność można sprawdzić, wyliczając możliwe modele, aż do znalezienia jednego, który spełnia zdanie. Problem określania spełnialności zdań w logice zdań – problem SAT – był pierwszym problemem, który okazał się NPzupełny. Wiele problemów w informatyce to tak naprawdę problemy spełnialności.
Trafność i spełnialność są oczywiście ze sobą powiązane: α jest poprawne, jeśli ¬α nie spełnia; przeciwnie, α jest spełnione jeśli ¬α jest nieważne. Mamy też następujący użyteczny wynik:
α |= β wtedy i tylko wtedy gdy zdanie (α Λ ¬β) jest niespełnione
Udowodnienie β z α poprzez sprawdzenie niespełnienia (α Λ ¬β) dokładnie odpowiada standardowej matematycznej technice dowodowej reductio ad absurdum (dosłownie „redukcja do rzeczy absurdalnej”). Nazywa się to również dowodem przez obalanie lub dowodem przez sprzeczność. Zakłada się, że zdanie β jest fałszywe i pokazuje, że prowadzi to do sprzeczności ze znanymi aksjomatami α. Ta sprzeczność jest dokładnie tym, co oznacza stwierdzenie, że zdanie (α Λ ¬β) jest niezadowalające.