Статья 483

Наиболее естественным для логической постановки задачи поиска доказательств оказалось секвенциальное исчисление. Несмотря на то, что секвенциальное исчисление, предложенное Г. Генценом в 1934 г. не было предназначено для решения проблем поиска доказательств, возможность построения доказательства снизу вверх, сведение задачи к подзадачам, имплицитно содержится в его работе. Решающий шаг был сделан в 1955 г. Я. Хинтиккой и Э.В. Бетом. Дело не только в чтении фигур заключения снизу вверх, но и во введении нового объекта - дерева поиска доказательств. Фигуры заключения целесообразно переформулировать так, как это было сделано в конце гл.1. Правило введения импликации слева - сформулировать в форме, предложенной А. Кетоненом
Правила введения слабых кванторов - в форме, предложенной С. Каягером.
Основными секвенциями будут секвенции вида. Структурных правил сокращения и добавления посылок нет.