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 secuencial clásico al generalizar la noción de estructura para permitir que la inferencia ocurra en contextos de alta complejidad estructural. El término inferencia profunda generalmente se reserva para los cálculos de demostración donde la complejidad estructural es ilimitada; en este artículo usaremos inferencia no superficial para referirnos a los cálculos que tienen una complejidad estructural mayor que el cálculo secuencial, pero no ilimitada, aunque esta no es una terminología establecida en la actualidad.
La inferencia profunda no es importante en lógica fuera de la teoría de la prueba estructural, ya que los fenómenos que conducen 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 ese momento.
Nuel Belnap propuso la lógica de visualización en un intento de caracterizar la esencia de la teoría de la prueba estructural. El cálculo de estructuras se propuso para dar una caracterización sin cortes de la lógica no conmutativa . El cálculo circular se desarrolló como un sistema de inferencia profunda que permitía dar cuenta explícitamente de la posibilidad de compartir subcomponentes.