В математической логике термин «глубокий вывод» обозначает общую идею в структурной теории доказательств , которая порывает с классическим секвенциальным исчислением , обобщая понятие структуры , чтобы разрешить вывод в контекстах высокой структурной сложности. Термин «глубокий вывод» обычно применяется к исчислениям доказательств , где структурная сложность неограниченна; в этой статье мы будем использовать термин «неповерхностный вывод» для обозначения исчислений, которые имеют структурную сложность большую, чем секвенциальные исчисления, но не неограниченно, хотя в настоящее время это не устоявшаяся терминология.
Глубокий вывод не важен в логике за пределами структурной теории доказательств, поскольку явления, которые приводят к предложению формальных систем с глубоким выводом, все связаны с теоремой об устранении сечения . Первое исчисление глубокого вывода было предложено Куртом Шютте [1] , но в то время эта идея не вызвала большого интереса.
Нуэль Белнап предложил логику отображения в попытке охарактеризовать сущность теории структурного доказательства. Исчисление структур было предложено для того, чтобы дать свободную от сечений характеристику некоммутативной логики . Циркуентное исчисление было разработано как система глубокого вывода, позволяющая явно учитывать возможность совместного использования подкомпонентов.