Теория доказательств
Формализация математических доказательств. Натуральный вывод (Генцен, 1935), секвенциальное исчисление. Нормализация: устранение обходных путей. Соответствие Карри-Ховарда: доказательства ≃ программы (1958/1969). Автоматизация: Coq, Lean (proof assistants).
Теория доказательств
Натуральный вывод и секвенции
Натуральный вывод описывает доказательство как последовательность локальных правил введения и устранения связок. Секвенциальное исчисление добавляет структурную дисциплину и анализ сечений.
Элиминация сечения
Элиминация сечения показывает, как удалить промежуточные леммы и получить конструктивное доказательство в секвенциальном исчислении. Это центральный механизм нормализации доказательств.