Verificación formal en acl2 de polinomios de múltiples variables y su aplicación al problema de la decisión en la lógica proposicional clásica

Abstract

This dissertation addresses the construction of formally verified libraries for multivariate polynomials within the framework provided by the ACL2 computational logic. Since ACL2 integrates a pure functional programming language and an automated reasoning system, these libraries can be used for both computation and formal reasoning on polynomial objects. The development of different variants of these objects allows us to explore increasingly constrained categories of abstract polynomials, enabling improvements in the underlying algorithms. In particular, regarding polynomials whose monomials form an integral domain or are endowed with a weakly admissible order, this leads to improvements in polynomial addition and multiplication algorithms. We develop a series of specializations to obtain executable polynomials for different domains from these abstract polynomials. Methodologically, a working style is adopted in which, when a domain is formalized, homonymous operations are defined in a different namespace. These new operations are normalizing, applying a normalization function to their arguments whose result is always in that domain. This normalization function gives rise to an induced equivalence relation that enables to transfer existing properties systematically, eliminating in the process those conditions related to the domain of the objects involved. This style is called "condition-free". One of those verified libraries formalizes multivariate Boolean polynomials. Starting from abstract Boolean monomials with an order and evaluation function, their operations and properties are presented. Then, the algorithms corresponding to these operations are refined to obtain improved versions, proving their equivalence to the original ones, and providing an evaluation homomorphism for Boolean polynomials. As an application of this verified library, we formalize a decision procedure for classical propositional logic from normalised Boolean polynomials, allowing the logical formulae to be represented in Zhegalkin normal form. Two algorithms are presented, one for deciding whether a formula is contradictory and one for deciding whether a formula is tautological. Soundness and completeness are formally proved, and we define functions that generate, where appropriate, models and counterexamples. Finally, the development effort is analysed using a series of metrics, presenting the results obtained for each library, discussing the factors that impact on the degree of automation and concluding with several work proposals on open research lines.