Статья 277

Имеется целый ряд очень интересных применений секвенциальных исчислений. Выводы в таких исчислениях суть конечные деревья секвенций, вершинами которых являются основные секвенции, а корнями - конечные или доказуемые секвенции. В силу свойств обратимости и подформульности правил, выводы в таких исчислениях с устранимым правилом сечения можно строить аналитически - снизу вверх, переходя от сложных формул рассматривая их как главные формулы некоторого правила к составляющим их подформулам боковым формулам.
Исчисления секвенций, хотя они первоначально и не были предназначены для этого, составили основу нового направления логического исследования поиска логических доказательств. Проиллюстрируем это на простом примере. Допустим, поставлена задача найти вывод формулы. Нам нужно установить, доказуема ли секвенция.