Verificación formal en ACL2 del algoritmo de Buchberger

Abstract

ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure lambda-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Grobner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in epsilon0-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied.