Título: Recuperando ‘fórmulas culpables’ de un lenguaje deóntico mediante el mapeo inverso de unsat cores
Director: Fernando Schapachnik
Jurados: Sergio Mera y Hernán Czemerinski

Resumen:

FormaLex es un conjunto de herramientas que tiene como objetivo modelar y analizar sistemas legales realizando de manera automatizada verificaciones de fórmulas lógicas que representan textos normativos. Como resultado de la ejecución, FormaLex determina si un documento normativo es consistente o si por el contrario se hallaron inconsistencias. En este proceso de verificación intervienen distintas herramientas, entre ellas se encuentra NuSMV que es un model checker utilizado como motor de razonamiento.

Este trabajo se centra principalmente en la interacción entre FormaLex y NuSMV, principalmente en la interpretación del output del mismo. El problema está relacionado con que actualmente el model checker al momento de responder que existe una contradicción no da indicios de cuáles son las fórmulas involucradas en la misma. En un trabajo previo llamado Recuperación de “fórmulas culpables” mediante análisis de unsat core de un trabajo previo se realizaron modificaciones a las herramientas que intervienen en el proceso de verificación de modelos, el model checker NuSMV y su interacción con el SAT solver Picosat. Dichas modificaciones permitieron formar un vínculo directo entre las variables del unsat core y las variables del model checker. Esta información brindada resulta valiosa para entender en dónde residen las inconsistencias, por lo que la propuesta de este trabajo en este aspecto consiste en tomar la información resultante de la extracción de unsat core y procesarla para identificar las variables de alto nivel involucradas en las fórmulas que hacen que un modelo legal no sea satisfacible.