Aproximaciones tratables acotadas en profundidad a la lógica proposicional intuicionista.

Ponente(s): Alejandro Javier Solares Rojas

El problema de decidir validez en lógica proposicional intuicionista (LPI) es PSPACE-completo [3] y, por tanto, intratable computacionalmente. Siendo así, no podemos esperar que un agente real, con recursos computacionales y cognitivos limitados, sea siempre capaz de reconocer en la práctica que una determinada conclusión se deriva de cierto conjunto de suposiciones. En este trabajo extendemos el enfoque de aproximaciones tratables “acotadas en profundidad” [e.g. 1, 2] a LPI: identificamos la fuente de la intratabilidad de LPI con el uso anidado de información hipotética involucrada al evaluar la verdad de fórmulas cuyo conectivo principal es el condicional o la negación, y consecuentemente introducimos un sistema de prueba híbrido (deducción natural + tableaux) para LPI que permite definir una jerarquía infinita de aproximaciones acotadas en profundidad a la misma. Específicamente, nuestro sistema: (i) está formulado mediante fórmulas signadas, donde los signos tienen una interpretación informacional intuitiva; (ii) consiste en reglas de introducción y eliminación lineales que fijan el significado de las conectivas, y en una única regla de ramificación que expresa un Principio de Bivalencia generalizado, es esencialmente una regla de corte analítico y regula el uso de información hipotética. A su vez, la profundidad de las inferencias se define como el número máximo permitido de aplicaciones anidadas de la regla de ramificación. La jerarquía resultante puede relacionarse naturalmente con el poder inferencial de agentes limitados en recursos, y el sistema de prueba subyacente es interesante en sí mismo ya que presenta una aceleración exponencial respecto a su sistema tableau contraparte [4]. Este trabajo se realiza con el apoyo del proyecto UNAM DGAPA PAPIIT IN101723, bajo el cual nos encontramos también desarrollando pruebas de normalización del sistema descrito arriba vía la correspondencia de Curry-Howard. [1] M. D’Agostino, M. Finger, and D. Gabbay. Semantics and proof-theory of depth bounded Boolean logics. Theoretical Computer Science, 480:43–68, 2013. [2] M. D’Agostino and A. Solares-Rojas. Tractable depth-bounded approximations to FDE and its satellites. Journal of Logic and Computation, exad040, 2023. [3] R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1):67–72, 1979. [4] A. Solares-Rojas. Tractable Depth-Bounded Approximations to some Propositional Logics. PhD Thesis, University of Milan, Milan, 2022.