Sekwenty Gentzena

Ten artykuł od 2011-07 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Sekwenty Gentzena – jeden z najprostszych sposobów automatycznego dowodzenia twierdzeń rachunku zdań. Został opracowany przez Gerharda Gentzena w 1934 roku. Znany jest również pod nazwą system LK od niemieckiej nazwy Logischer Kalkül. Jest to jednocześnie jedna z formalizacji rachunku predykatów.

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ą (M ∧ N) 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 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.