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 {ai} poprzedników i zbioru {bj} następników, połączonych zależnością (którą mamy udowodnić) – jeśli wszystkie ai są prawdziwe, to któreś z bi 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