La inferencia profunda nombra una idea general en la teoría de la prueba 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 cálculos de prueba donde la complejidad estructural es ilimitada; en este artículo usaremos inferencia no superficial para referirnos a cálculos que tienen una complejidad estructural mayor que el cálculo posterior, pero no sin límites, 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 exhibició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 libre de cortes de la lógica no conmutativa . El cálculo circular se desarrolló como un sistema de inferencia profunda que permite explicar explícitamente la posibilidad de compartir subcomponentes.
Notas
- ^ Kurt Schütte. Teoría de la prueba. Springer-Verlag, 1977.
Otras lecturas
- Kai Brünnler, "Deep Inference and Symmetry in Classical Proofs" ( tesis doctoral 2004 ), también publicado en forma de libro por Logos Verlag ( ISBN 978-3-8325-0448-9 ).
- Inferencia profunda y cálculo de estructuras Introducción y página web de referencia sobre la investigación en curso en inferencia profunda.