Sekwenty Gentzena

Z Wikipedii

Sekwenty Gentzena to jeden z najprostszych sposobów automatycznego dowodzenia twierdzeń rachunku zdań. Został opracowany przed Gerharda Gentzena.

Każdy sekwent składa się ze zbioru {a_i} poprzedników i zbioru {b_j} następników, połączonych zależnością (którą mamy udowodnić):

jeśli wszystkie a_i są prawdziwe, to któreś z b_i jest prawdziwe

Dowodzenie zaczyna się od jednego sekwentu z pustym zbiorem poprzedników i zbiorem następników składających się z twierdzenia które zamierzamy udowodnić.

Wykonujemy następujące kroki:

złożone zależności, takie jak implikacja, równoważność itd. zastępujemy alternatywami, koniunkcjami i negacjami
następnik będący alternatywą (M ∨ N) zastępujemy dwoma następnikami: M, N
poprzednik będący koniunkcją (p ∧ q) zastępujemy dwoma poprzednikami: M, N
następnik będący negacją (¬ M) zastępujemy poprzednikiem bez negacji: M
poprzednik będący negacją (¬ M) zastępujemy następnikiem bez negacji: M
jeśli kilka następników jest identycznych można zachować tylko jeden z nich
jeśli kilka poprzedników jest identycznych można zachować tylko jeden z nich
jeśli następnik jest koniunkcją (M ∧ N) zamieniamy sekwent na dwa, o tych samych poprzednikach, i 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 następniku (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 twierdzednie jest prawdziwe.