Inferencia profunda

En lógica matemática , la inferencia profunda designa una idea general en la teoría de la demostración estructural que rompe con el cálculo de secuentes clásico al generalizar la noción de estructura para permitir la inferencia en contextos de alta complejidad estructural. El término inferencia profunda se suele reservar para cálculos de demostración cuya complejidad estructural es ilimitada; en este artículo utilizaremos inferencia no superficial para referirnos a cálculos cuya complejidad estructural es mayor que la del cálculo de secuentes, pero no ilimitada, aunque esta terminología no está actualmente establecida.

La inferencia profunda no es importante en lógica fuera de la teoría de la demostración estructural, ya que los fenómenos que llevan a la propuesta de sistemas formales con inferencia profunda están todos relacionados con el teorema de eliminación de cortes . El primer cálculo de inferencia profunda fue propuesto por Kurt Schütte , ^{[ 1 ]} pero la idea no generó mucho interés en su momento.

Nuel Belnap propuso la lógica de visualización en un intento por caracterizar la esencia de la teoría de la demostración estructural. El cálculo de estructuras se propuso para ofrecer una caracterización sin cortes de la lógica no conmutativa . El cálculo de circunscripciones se desarrolló como un sistema de inferencia profunda que permite tener en cuenta explícitamente la posibilidad de compartir subcomponentes.

• Kai Brünnler, «Inferencia profunda y simetría en demostraciones clásicas» ( tesis doctoral, 2004, archivada el 8 de diciembre de 2006 en Wayback Machine ), también publicada en formato de libro por Logos Verlag ( ISBN 978-3-8325-0448-9).
• Inferencia profunda y el cálculo de estructuras: Introducción y página web de referencia sobre la investigación en curso en inferencia profunda.
• Aler Tubella, Andrea; Straßburger, Lutz (2019). Introducción a la inferencia profunda: notas de clase para ESSLLI'19, 5-16 de agosto de 2019, Universidad de Letonia (PDF) (Informe).