Teoría computacional (en ACL2) sobre cálculos proposicionales

Resumen

En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2, También se analizan las características comunes a determinados cálculos bien conocidos, definiendo un marco genérico del que son casos particulares. El trabajo comienza con la formalización de la lógica proposicional, para la que se consideran dos semánticas, la clásica y la semántica trivalorada fuerte de Kleene. Una vez hecho esto, se desarrollan procedimientos de decisión de satisfacibilidad, validez y consecuencia lógica (tanto en la semántcia clásica como en la de Kleene) basados en el cálculo de los tableros semánticos y el cálculo de secuentes. Se proporcionan implementaciones verificadas de estos procedimientos. A partir de estos dos métodos de decisión de satisfacibilidad se define un marco genérico que abstrae sus características comunes: los Sistemas de Transformación Proposicionales. Esta abstracción permite desarrollar procedimientos de decisión de satisfacibilidad a partir de un conjunto de reglas de transformación con determinadas propiedades básicas. La implementación del marco genérico se puede instanciar para construir de forma automática procedimientos verificados de decisión de satisfacibilidad. Se muestra cómo se realiza esta instancia para los métodos basados en tableros semánticos y en secuentes. El desarrollo del marco genérico se ha realizado tanto para la semántica clásica como para la semántcia de Kleene. A continuación se desarrollan otros procedimientos de decisión de satisfacibilidad, analizando la posibilidad de expresarlos como sistemas de transformación proposicionales. Esto ocurre con el procedimiento de Davis y Putnam, el cual es desarrollado primero de forma independiente al marco genérico y después se expresa como una instancia del mismo.