następniku (M ∧ N) zastąpionym odpowiednio przez M i N; analogicznie, jeśli poprzednik jest alternatywą (M ∨ N) zamieniamy sekwent na dwa, o tych samych następnikach, i poprzedniku (M ∨ N) zastąpionym odpowiednio przez M i N; jeśli wszystkie następniki i poprzedniki sekwentu są zmiennymi zdaniowymi i żadna z nich nie występuje jednocześnie w następniku i poprzedniku, twierdzenie jest fałszywe; jeśli wszystkie następniki i poprzedniki sekwentu są zmiennymi zdaniowymi i chociaż jedna z nich występuje jednocześnie w następniku i poprzedniku, sekwent jest poprawny i przystępujemy do analizy kolejnego sekwentu; jeśli był to już ostatni sekwent twierdzenie jest prawdziwe.
Przykład działania: {}, {p ∨ ¬ p} – rozbijamy alternatywę w następniku {}, {p, ¬ p} – przenosimy negację na drugą stronę {p}, {p} – zmienna p się powtarza prawda
W logice pierwszego rzędu można pokazać zupełność i poprawność systemu Gentzena.
Linki zewnętrzne
Kategoria:Automatyczne dowodzenie twierdzeń