Просмотр кода страницы Исчисление секвенций

'''Исчисление секвенций''' — вариант [[Логическое исчисление|логических исчислений]], использующий для доказательства утверждений не произвольные цепочки [[Тавтология (логика)|тавтологий]], а последовательности условных суждений — секвенций{{Переход|#Секвенци}}. Наиболее известные исчисления секвенций — <math>\mathbf{LK}</math>{{переход|#Классическое генценовское исчисление секвенций}} и <math>\mathbf{LJ}</math>{{переход|#Интуиционистское генценовское исчисление секвенций}} для классического и интуиционистского исчислений предикатов — построены [[Генцен, Герхард|Генценом]] в [[1934 год в науке|1934 году]], позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.

В секвенциальном подходе вместо широких наборов [[аксиома|аксиом]] используются развитые системы [[Правило вывода|правил вывода]], а [[Математическое доказательство|доказательство]] ведётся в форме дерева вывода; по этому признаку (наряду с системами [[натуральный вывод|натурального вывода]]) исчисления секвенций относятся к [[исчисление генценовского типа|генценовскому типу]], в противоположность аксиоматическим {{iw|исчисление гильбертовского типа|гильбертовским исчислениям|en|Hilbert system}}, в которых при развитом наборе аксиом количество правил вывода сведено к минимуму.

Основное свойство секвенциальной формы — симметричное устройство{{переход|#Симметрия}}, обеспечивающее удобство доказательства [[Устранимость сечений|устранимости сечений]], и, как следствие, исчисления секвенций являются основными исследуемыми системами в [[Теория доказательств|теории доказательств]].

== История ==
Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в [[1929 год в науке|1929 году]] немецкий физик и логик {{нп2|Герц, Пауль|Пауль Герц|de|Paul Hertz (Physiker)|Paul Hertz|text=1881–1940}}<ref>{{статья | автор = Hertz P. | заглавие = Über Axiomensysteme für beliebige Satzsysteme | ссылка = https://archive.org/details/sim_mathematische-annalen_1929_101/page/457 | издание = Mathematische Annalen
| том = 101 | страницы = 457–514 | год = 1929 | язык = de | doi = 10.1007/BF01454856}}</ref>, но целостного исчисления для какой-либо логической теории в его трудах построено не было{{sfn|Инджейчак|2014|p=1310|loc=Hertz did not present any specific system for concrete logic. His approach was abstract; he defined rather a schema of the system in which the only rules have purely structural character}}. В работе 1932 года Генцен попытался развить подход Герца<ref>{{статья | автор = Gentzen G. | заглавие = Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen | издание = Mathematische Annalen | том = 107 | страницы = 329–350 | год = 1932 | язык = de | doi = 10.1007/BF01448897}}</ref>, но в 1934 году отказался от наработок Герца: ввёл системы [[натуральный вывод|натурального вывода]] <math>\mathbf{NK}</math> и <math>\mathbf{NJ}</math> для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы <math>\mathbf{LK}</math> и <math>\mathbf{LJ}</math>. Для <math>\mathbf{LK}</math> и <math>\mathbf{LJ}</math> Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал [[Полная теория|полноту]] интуиционистского исчисления предикатов, а в [[1936 год в науке|1936 году]] — доказал [[непротиворечивость]] [[Аксиоматика Пеано|аксиоматики Пеано]] для целых чисел, расширив её с помощью секвенциального варианта <math>\mathbf{NK}</math> [[Трансфинитная индукция|трансфинитной индукцией]] до [[Порядковое число|ординала]] <math>\epsilon_0</math>. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с [[Теорема Гёделя о неполноте|теоремой Гёделя о неполноте]], согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в [[1944 год в науке|1944 году]] {{нп2|Кетонен, Ойва|Ойвой Кетоненом|fi|Oiva Ketonen|text=1913—2000}} исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости{{Sfn|Ян фон Плато|2008}}<ref>{{статья | автор = [[Бернайс, Пауль|Bernays P.]] | заглавие = Review: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul | издание = [[Journal of Symbolic Logic]] | том = 10 | номер = 4 | страницы = 127—130 | год = 1945 | язык = en | ссылка = https://philpapers.org/rec/BERROK | archivedate = 2019-01-21 | archiveurl = https://web.archive.org/web/20190121064246/https://philpapers.org/rec/BERROK }}</ref>. Опубликованное в 1949 году в диссертации [[Сушко, Роман (логик)|Романа Сушко]] безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа<ref>{{статья | автор = Suszko R. | заглавие = Formalna teoria wartości logicznych | издание = Studia Logica | том = 6 | страницы = 145–320 | год = 1957 | язык = pl}}</ref>{{sfn|Инджейчак|2014|p=1310|loc=1310—1315}}.

В [[1952 год в науке|1952 году]] [[Стивен Клини]] во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода{{Sfn|Клини|1958|с=389—406}}, там же ввёл исчисления генценовского типа <math>G3i</math> и <math>G3c</math>, в которых не требовались структурные{{Переход|#Структурное правило вывода}} правила вывода{{Sfn|Клини|1958|с=424—434}}, и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов{{Sfn|Ян фон Плато|2008}}.

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, [[теория типов|теории типов]], [[Неклассическая логика|неклассические логики]]. В [[1953 год в науке|1953 году]] {{нп2|Такеути, Гаиси|Гаиси Такеути|ja|竹内外史|text=1926—2017}} построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений ([[гипотеза Такеути]]). В [[1966 год в науке|1966 году]] {{нп2|Тэйт, Уильям|Уильям Тэйт|en|William W. Tait|род. 1929}} доказал устранимость сечений для [[Логика второго порядка|логики второго порядка]], вскоре гипотеза была полностью доказана в работах [[Такахаси, Мотоо|Мотоо Такахаси]]<ref>{{статья | автор = Takahashi M. | заглавие = A proof of cut-elimination theorem in simple type-theory | издание = Journal of Japanese Mathematical Society | том = 19 | номер = 4 | год = 1967 | страницы = 399—410 | ссылка = https://projecteuclid.org/euclid.jmsj/1260478312 | doi = 10.2969/jmsj/01940399 | archivedate = 2019-01-21 | archiveurl = https://web.archive.org/web/20190121064307/https://projecteuclid.org/euclid.jmsj/1260478312 }}</ref> и {{нп2|Правиц, Даг|Дага Правица|sv|Dag Prawitz|text=род. 1936}}. В 1970-е годы результаты значительно расширены: [[Драгалин, Альберт Григорьевич|Драгалиным]] найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а {{iw|Жирар, Жан-Ив|Жирар|fr|Jean-Yves Girard}} — для [[Система F|системы F]].

Начиная с 1980-х годов секвенциальные системы играют ключевую роль в развитии систем [[Автоматическое доказательство|автоматического доказательства]], в частности, разработанное [[Кокан, Тьерри|Тьерри Коканом]] и [[Юэ, Жерар|Жераром Юэ]] в 1986 году секвенциальное [[исчисление конструкций]] — [[Полиморфизм (программирование)|полиморфное]] [[λ-исчисление]] высшего порядка с [[Зависимый тип|зависимыми типами]], занимающее высшую точку в [[Лямбда-куб|λ-кубе Барендрегта]] — используется как основа программной системы [[Coq]].

== Основные понятия ==
{{якорь|Секвенция|Цедент}}'''''Секвенцией''''' называется выражение вида <math>\Gamma \rightarrow \Delta</math>, где <math>\Gamma</math> и <math>\Delta</math> — конечные (возможно пустые) последовательности логических формул, называемые '''''цедентами''''': <math>\Gamma</math> — [[антецедент]]ом, а <math>\Delta</math> — [[сукцедент]]ом (иногда — [[консеквент]]ом). Интуитивный смысл, закладываемый в секвенцию <math>A_1, \ldots, A_n \rightarrow B_1, \ldots, B_m</math> — если выполнена [[конъюнкция]] формул антецедента <math>A_1 \land \ldots \land A_n</math>, то имеет место (выводится) [[дизъюнкция]] формул сукцедента <math>B_1 \lor \ldots \lor B_m</math>. Иногда вместо стрелки в обозначении секвенции используется знак выводимости (<math>\Gamma \vdash \Delta</math>) или знак импликации (<math>\Gamma \Rightarrow \Delta</math>).

{{якорь|Пустая секвенция}}Если антецедент пуст (<math>\rightarrow B_1, \ldots, B_m</math>), то подразумевается выполнение дизъюнкции формул сукцедента <math>B_1 \lor \ldots \lor B_m</math>; пустой сукцедент (<math>A_1, \ldots, A_n \rightarrow</math>) интерпретируется как противоречивость конъюнкции формул антецедента. '''''Пустая секвенция''''' <math>\rightarrow</math> означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде <math>A, \Gamma</math> или <math>\Gamma, A</math>, где <math>\Gamma</math> — последовательность формул, а <math>A</math> — формула, означает добавление формулы <math>A</math> в цедент (возможно, в ещё одном экземпляре).

[[Аксиома]]ми считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях <math>\mathrm{LK}</math> и <math>\mathrm{LJ}</math> задаётся только одна схема аксиом — <math>A \rightarrow A</math>. [[Правила вывода]] в секвенциальной форме записываются как следующие выражения:
: <math>\cfrac{\;S_1\;}{T}</math> и <math>\cfrac{\;S_1 \;\;\; S_2\;}{\;\;T}</math>,
интерпретируются они как утверждение о выводимости из верхней секвенции <math>S_1</math> (верхних секвенций <math>S_1</math> и <math>S_2</math>) нижней секвенции <math>T</math>. Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:
: <math>\cfrac{\cfrac{\;S_1 \;\;\; S_2\;}{\;T_1} \;\;\;\; \cfrac{\;S_3\;}{T_2}}{U}</math>,
где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции <math>S</math>, означает её выводимость в данной логической системе: <math>\vDash S</math>.

== Классическое генценовское исчисление секвенций ==
Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система <math>\mathbf{LK}</math>, построенная Генценом в 1934 году. В системе одна схема аксиом — <math>A \rightarrow A</math> и 21 правило вывода, которые делятся на структурные и логические{{Sfn|Такеути|1978|сс=15—17}}.

{{Якорь|Структурное правило вывода}}'''''Структурные правила''''' (<math>A</math>, <math>B</math> — формулы, <math>\Gamma</math>, <math>\Delta</math>, <math>\Theta</math>, <math>\Lambda</math> — списки формул):
* ослабление слева: <math>\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A, \ \Gamma \ \rightarrow \ \Delta}</math> и справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta \quad}{\ \Gamma \ \rightarrow \ \Delta, \ A}</math>;
* сокращение слева: <math>\cfrac {\,\, A, \ A, \ \Gamma \ \rightarrow \ \Delta}{\qquad  A, \ \Gamma \ \rightarrow \ \Delta \ }</math> и справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A, \ A}{\,\,\, \Gamma \ \rightarrow \ \Delta, \ A \qquad}</math>;
* перестановка слева: <math>\cfrac {\ \Gamma, \ A, \ B, \ \Theta \ \rightarrow \ \Delta \ }{\ \Gamma, \ B, \ A, \ \Theta \ \rightarrow \ \Delta}</math> и справа: <math>\cfrac {\ \Gamma \ \rightarrow \ \Delta, \ A, \ B, \ \Lambda \ }{\ \Gamma \ \rightarrow \ \Delta, \ B, \ A, \ \Lambda \ }</math>,
* [[Сечение (теория доказательств)|сечение]]: <math>\cfrac {\ \Gamma \ \rightarrow \ \Delta, \ A \qquad A, \ \Theta \ \rightarrow \ \Lambda \ }{\Gamma, \ \Theta \ \rightarrow \ \Delta, \ \Lambda }</math>.

Логические пропозициональные правила предназначены для добавления в вывод [[Пропозициональная связка|пропозициональных связок]]:
* <math>\lnot</math>-слева: <math>\cfrac {\qquad \Gamma \ \rightarrow \ \Delta, \ A}{\ \lnot A, \ \Gamma \ \rightarrow \ \Delta \qquad}</math>; <math>\lnot</math>-справа: <math>\cfrac {A, \ \Gamma \ \rightarrow \ \Delta \qquad}{\qquad \Gamma \ \rightarrow \ \Delta, \ \lnot A \ }</math>;
* <math>\land</math>-слева: <math>\cfrac {\qquad A, \ \Gamma \ \rightarrow \ \Delta }{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }</math> и <math>\cfrac {\qquad B, \ \Gamma \ \rightarrow \ \Delta}{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }</math>; <math>\land</math>-справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad \Gamma \ \rightarrow \ \Delta, \ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta, \ A\land B \ } </math>,
* <math>\lor</math>-слева: <math>\ \cfrac {A, \ \Gamma \ \rightarrow \ \Delta \qquad B, \ \Gamma \ \rightarrow \ \Delta \ }{\ A \lor B, \ \Gamma \ \rightarrow \ \Delta \ \qquad}</math>; <math>\lor</math>-справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad}{\ \Gamma \ \rightarrow \ \Delta, \ A \lor B \ }</math> и <math>\cfrac {\Gamma \rightarrow \Delta, \ B \qquad}{\ \Gamma \rightarrow \Delta, \ A \lor B \ }</math>,
* <math>\Rightarrow</math>-слева: <math>\ \cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad \qquad B, \ \Theta \ \rightarrow \ \Lambda \ }{A \Rightarrow B, \ \Gamma, \ \Theta \ \rightarrow \ \Delta, \Lambda\qquad}</math> и <math>\Rightarrow</math>-справа: <math>\cfrac {A, \ \Gamma \ \rightarrow \ \Delta, \ B \qquad }{\qquad \Gamma \ \rightarrow \ \Delta, \ A \Rightarrow B \ }</math>.

Логические кванторные правила вводят кванторы [[Квантор всеобщности|всеобщности]] и [[Квантор существования|существования]] в вывод (<math>F(a)</math> — формула со свободной переменной <math>a</math>, <math>t</math> — произвольный терм, а <math>F(t)</math> — замена всех вхождений свободной переменной <math>a</math> на терм <math>t</math>):
* <math>\forall</math>-слева: <math> \cfrac {\qquad F(t), \ \Gamma \ \rightarrow \ \Delta}{\ \forall x : F(x), \ \Gamma \ \rightarrow \ \Delta \ }</math> и <math>\forall</math>-справа: <math> \cfrac {\Gamma \ \rightarrow \ \Delta, \ F(a) \qquad}{\ \Gamma \ \rightarrow \ \Delta, \ \forall x : F(x)}</math>;
* <math>\exists</math>-слева: <math> \cfrac {\qquad F(a), \ \Gamma \ \rightarrow \ \Delta}{\ \exists x : F(x), \ \Gamma \ \rightarrow \ \Delta \ }</math> и <math>\exists</math>-справа: <math> \cfrac {\Gamma \ \rightarrow \ \Delta, \ F(t) \qquad}{\ \Gamma \ \rightarrow \ \Delta, \ \exists x : F(x)}</math>.
Дополнительное условие в кванторных правилах — невхождение свободной переменной <math>a</math> в нижние формулы секвенций в правилах <math>\forall</math>-справа и <math>\exists</math>-слева.

Пример <math>\mathbf{LK}</math>-вывода [[Закон исключённого третьего|закона исключённого третьего]]:
: <math>\cfrac{\cfrac{\cfrac{\cfrac{\cfrac
        {A \ \rightarrow \ A \qquad}
        {\qquad \quad \rightarrow \ A, \ \lnot A \qquad }}
	{\qquad \qquad \rightarrow \ A, \ A \lor \lnot A \quad }}
	{\qquad \quad \rightarrow \ A \lor \lnot A, \ A}}
        {\qquad\qquad\qquad \ \rightarrow \ A \lor \lnot A, \ A \lor \lnot A \quad}}
	{\quad \ \rightarrow \ A \lor \lnot A}</math>
— в нём вывод начат с единственной аксиомы, далее — последовательно применены правила <math>\lnot</math>-справа, <math>\lor</math>-справа, перестановка справа, <math>\lor</math>-справа и сокращение справа.

Исчисление <math>\mathbf{LK}</math> эквивалентно классическому исчислению предикатов первой ступени: формула <math>A</math> общезначима в исчислении предикатов тогда и только тогда, когда в <math>\mathbf{LK}</math> выводима секвенция <math>\rightarrow A</math>. Ключевой результат, который назван Генценом «[[Основная теорема|основной теоремой]]» ({{lang-de|Hauptsatz}}) — возможность провести любой <math>\mathbf{LK}</math>-вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства <math>\mathbf{LK}</math>, в том числе [[корректность (логика)|корректность]], [[непротиворечивость]] и полнота.

== Интуиционистское генценовское исчисление секвенций ==
Исчисление <math>\mathbf{LJ}</math> получается из <math>\mathbf{LK}</math> добавлением ограничения на сукцеденты секвенций в правилах вывода: в них допустимо использование только одной формулы, а правила перестановки справа и сокращения справа (оперирующие с нескольким формулами в сукцедентах) исключаются. Таким образом, при минимальных модификациях получается система, в которой невыводимы законы [[Двойное отрицание|двойного отрицания]] и [[закон исключённого третьего|исключённого третьего]], но действуют все прочие основные логические законы, и, например, выводима эквивалентность <math>\lnot \lnot \lnot A \Leftrightarrow \lnot A</math>. Полученная система эквивалентна [[Интуиционизм|интуиционистскому]] исчислению предикатов с [[Интуиционистское исчисление высказываний|аксиоматикой Гейтинга]]. В исчислении <math>\mathbf{LJ}</math> также устранимы сечения, оно также корректно, непротиворечиво и полно, притом последний результат для интуиционистского исчисления предикатов впервые получен именно для <math>\mathbf{LJ}</math>.

== Нестандартные исчисления секвенций ==
Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система {{нп2|Саппс, Патрик|Саппса|en|Patrick Suppes|text=1922–2014}} 1957 года<ref>{{книга | автор = Suppes P. | заглавие = Introduction to Logic | издательство = Van Nostrand | место = Princeton | год = 1957 }}</ref> (почерпнутая из замечаний {{iw|Фейс, Роберт|Фейса|en|Robert Feys}} и {{iw|Ладриэр, Жан|Ладриера|fr|Jean Ladrière}} к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году {{нп2|Леммон, Джон|Леммоном|en|John Lemmon|text=1930–1966}}<ref>{{книга | автор = Lemmon E. J. | заглавие = Beginning Logic | издательство = Nelson | место = London | год = 1965}}</ref>, устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена{{sfn|Инджейчак|2014|p=1300}}. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены {{нп2|Хермес, Ханс|Хермесом|de|Hans Hermes|text=1912–2003}}<ref>{{книга | автор = Hermes H. | заглавие = Einführung in die Mathematische Logik | издательство = Teubner | место = Stuttgart | год = 1963}}</ref>: в его системе для классической логики применены две аксиомы (<math>A \rightarrow A</math> и <math>\rightarrow A = A</math>, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях{{sfn|Инджейчак|2014|p=1300|loc= <...> in order to obtain more flexible tool for actual proof search one can admit the possibility of making logical operations also in antecedents. <…> It seems that the first system of this sort was provided by Hermes. He also uses intuitionistic sequents with sequences of formulae in antecedents in his formalization of classical logic with identity. As primitive sequents Hermes uses only: <math>\varphi \Rightarrow \varphi</math> and <math>\Rightarrow \tau = \tau</math>}}.
{{дополнить раздел|дата=2019-01-24}}

== Симметрия ==
Секвенциальным исчислениям присуща симметрия, естественно выражающая [[двойственность (математическая логика)|двойственность]], в аксиоматических теориях формулируемую [[Законы де Моргана|законами де Моргана]].
{{дополнить раздел|дата=2019-01-20}}

== Примечания ==
{{примечания}}

== Литература ==
* {{БСЭ3|статья=Секвенций исчисление | том=23 | страницы = 181—182; ст. 530—532 | ref = БСЭ}}
* {{Книга:Математическая энциклопедия | 4 | автор = [[Драгалин, Альберт Григорьевич|Драгалин А. Г.]] | статья = Секвенций исчисление | страницы = 1104 | ref = Математическая энциклопедия | eom = Sequent calculus}}
* {{Источник/НФЭ|Исчисление секвенций|Быстров П. И.}}
* {{статья | автор = Генцен Г. | заглавие = Исследования логических выводов | оригинал = <small>Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431</small> | ответственный = перевод А. В. Идельсона | автор издания = Идельсон А. В., Минц Г. Е. | издание = Математическая теория логического вывода | место = М. | издательство = Наука | год = 1967 | страницы = 9—76}}
* {{книга | автор = Драгалин А. Г. | заглавие = Математический интуиционизм. Введение в теорию доказательств| место = М. | издательство = [[Наука (издательство)|Наука]] | год = 1979 | страниц = 256 | серия = Математическая логика и основания математики | ref = Драгалин}}
* {{книга | автор = Клини С. | заглавие = Введение в метаматематику | место = М. | издательство = ИЛ | год = 1958 | ответственный = перевод с английского [[Есенин-Вольпин, Александр Сергеевич|А. С. Есенина-Вольпина]] под редакцией [[Успенский, Владимир Андреевич|В. А. Успенского]] | страниц = 527 | ref = Клини}}
* {{книга | автор = Такеути Г. | заглавие = Теория доказательств | место = М. | издательство = Мир | год = 1978 | страниц = 412 | ref = Такеути}}
* {{статья | автор = Indrzejczak A. | заглавие = A Survey of Nonstandard Sequent Calculi | издание = {{iw|Studia Logica}} | год = 2014 | месяц = December | том = 102 | номер = 6 | страницы = 1295–1322 | doi = 10.1007/s11225-014-9567-y | ref = Инджейчак}}
* {{cite web | url = https://plato.stanford.edu/entries/proof-theory-development/ | author = Jan von Plato | title = The Development of Proof Theory | work = [[Stanford Encyclopaedia of Philosophy]] | date = 2008-04-16 | ref = Ян фон Плато2008}}

{{ВС}}
{{Логика}}

[[Категория:Теория доказательств]]
[[Категория:Автоматическое доказательство теорем]]