		Search-engine friendly clone of the ACL2 documentation.

Pubs-papers

Pubs-logic-and-metamathematics

Logic and Metamathematics

Formal Correctness of a Quadratic Unification Algorithm, J.L. Ruiz-Reina, F.J. Martin-Mateos, J.A. Alonso and M.J. Hidalgo. Journal of Automated Reasoning (37):1-2, pp. 67-92, 2006. The paper presents the formal verification of a syntactic unification algorithm of quadratic time complexity, using a dag representation for terms. The use of stobjs and defexec/mbe makes the algorithm efficiently executable.
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2, F.J. Martin-Mateos, J.L. Ruiz-Reina, J.A. Alonso and M.J. Hidalgo. Journal of Automated Reasoning (47):3, pp. 229-250, 2011. Highman's Lemma is a property about well quasi-orderings on strings. In this paper a formal proof of this result is presented, using a termination argument based on well-founded multiset extensions.
A Formal Proof of Dickson's Lemma in ACL2, F.J. Martin-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. LPAR 2003 - LNAI 2850, pp. 49-58, 2003. Dickson's Lemma is the main result needed for proving termination of Buchberger's algorithm for computing Groebner basis of ideals of polynomials. In this paper a formal proof of this result is presented, using a termination argument based on well-founded multiset extensions.
Formal verification of a generic framework to synthesize SAT-provers, F.J. Martin-Mateos, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz-Reina. Journal of Automated Reasoning (32):4, pp. 287-313, 2004. A generic framework for SAT checkers is defined and verified. Several verified and executable SAT solvers can be obtained instantiating this generic framefork.
Termination in ACL2 Using Multiset Relations, J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Martin-Mateos. Thirty Five Years of Automating Mathematics, pp. 217-245. 2003. A proof in ACL2 of the well-foundedness of multiset extensions of well-founded relations and a tool for generating automatically such multiset relations.
A certified polynomial-based decision procedure for propositional logic , I. Medina Bulo, F. Palomo Lozano and J. A. Alonso Jimenez, 4th International Conference on Theorem Proving in Higher Order Logics , LNCS 2152:297-312. Edinburgh (Escocia), 2001. In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. This formalization is suitable for its automatic verification in an applicative logic like ACL2. This application of polynomials has been developed by reusing a previous work on polynomial rings, showing that a proper formalization leads to a high level of reusability. Two checkers are defined: the first for contradiction formulas and the second for tautology formulas. The main theorems state that both checkers are sound and complete. Moreover, functions for generating models and counterexamples of formulas are provided. This facility plays also an important role in the main proofs. Finally, it is shown that this allows for a highly automated proof development.
Formal Proofs About Rewriting Using ACL2, J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Martin-Mateos. Annals of Mathematics and Artificial Intelligence 36(3), pp. 239-262, 2002. This paper presents a formalization of term rewriting systems. That is, ACL2 is used as the metatheory to formalize results in equational reasoning and rewrite systems. Notions such as confluence, local confluence, and normal forms are formalized. The main theorems proved are Newman's Lemma and Knuth-Bendix critical-pair theorem.
Ivy: A Preprocessor and Proof Checker for First-Order Logic, William McCune and Olga Shumsky, Chapter 16 of Computer-Aided Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000. (ACL2 scripts are available from directory 1999/ivy/ in the community-books.) In this case study, a proof checker for first-order logic is proved sound for finite interpretations. In addition, the study shows how non-ACL2 programs can be combined with ACL2 functions in such a way that useful properties can be proved about the composite programs. Nothing is proved about the non-ACL2 programs. Instead, the results of the non-ACL2 programs are checked at run time by ACL2 functions, and properties of these checker functions are proved. The ACL2 scripts referenced here provide the full details of the results described in the article along with solutions to all the exercises in the article.