Натуральный вывод и секвенции

Натуральный вывод описывает доказательство как последовательность локальных правил введения и устранения связок. Секвенциальное исчисление добавляет структурную дисциплину и анализ сечений.