Глубокий вывод

В математической логике глубокий вывод обозначает общую идею теории структурных доказательств , которая порывает с классическим секвенциальным исчислением , обобщая понятие структуры , чтобы сделать вывод возможным в контекстах высокой структурной сложности. Термин «глубокий вывод» обычно применяется к исчислениям доказательств , структурная сложность которых неограничена; в этой статье мы будем использовать неповерхностный вывод для обозначения исчислений, структурная сложность которых превышает структурную сложность секвенциального исчисления, но не без ограничений, хотя в настоящее время это не устоявшаяся терминология.

Глубокий вывод не важен в логике за пределами теории структурных доказательств, поскольку все явления, которые приводят к предложению формальных систем с глубоким выводом, связаны с теоремой об исключении разреза . Первое исчисление глубокого вывода было предложено Куртом Шютте . но в то время эта идея не вызвала особого интереса.

Нуэль Белнап предложил логику отображения , пытаясь охарактеризовать сущность теории структурных доказательств. Исчисление структур было предложено для того, чтобы дать характеристику некоммутативной логики без разрезов . Цирквентное исчисление было разработано как система глубокого вывода, позволяющая явно учитывать возможность совместного использования подкомпонентов.

Дальнейшее чтение

• Кай Брюннлер, «Глубокий вывод и симметрия в классических доказательствах» ( докторская диссертация, 2004 г. ), также опубликованная в виде книги издательством Logos Verlag ( ISBN   978-3-8325-0448-9 ).
• Глубокий вывод и исчисление структур Введение и справочная веб-страница о текущих исследованиях в области глубокого вывода.