Se ha publicado un artículo de automatización del razonamiento titulado Exploring theories with a model-finding assistant.
Sus autores son Salman Saghafi, Ryan Danas y Daniel J. Dougherty (del Applied Logic and Security Lab en el Worcester Polytechnic Institute, Worcester, Massachusetts, USA).
Su resumen es
We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances.
Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models.
Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.
El trabajo se ha presentado en el CADE-25 (The 25th International Conference on Automated Deduction).
El código en Haskell del sistema Razor se encuentra aquí.
Este trabajo puede servir en los cursos de Lógica informática, Lógica matemática y fundamentos, Razonamiento automático y Lógica computacional y teoría de modelos.