Глава VIII. Исчисления секвенций.   Исчисление секвенций (от англ. Sequent calculus) — система формального вывода формул логики первого порядка предложенная немецким логиком Герхардом Генценом. Генценом были разработаны несколько эквивалентных вариантов исчисления секвенций. Секвенциальные формулы представляют собой последовательность, разделенную знаком выводимости «⊦», в которой слева (в антецеденте) находится дизъюнктивная последовательность, а справа (в консеквенте, или в … Читать далее VIII. Исчисления секвенций