Verified Computer Algebra in ACL2 - Artificial Intelligence and Symbolic Computation - page 172

logic, less expressive 1 than the logic of Coq, which is based on type theory. We
show how it is possible to formalize all the needed theory within the Acl2 logic.
The formal proofs developed in Acl2 are mainly adapted from Chap. 8 of [1].
As the whole development consists of roughly one thousand Acl2 theorems and
function definitions, we will only scratch its surface presenting the main results
and a sketch of how the pieces fit together. We will necessarily omit many details
that, we expect, can be inferred from the context.

2 The Acl2 System

Acl2 formalizes an applicative subset of Common Lisp. In fact, the same lan-
guage, based on prefix notation, is used for writing Lisp code and stating the-
orems about it 2 . The logic is a quantifier-free fragment of first-order logic with
equality. It includes axioms for propositional logic and for a number of Lisp
functions and data types. Inference rules include those for propositional calcu-
lus, equality and instantiation (variables in formulas are implicitly universally
quantified). One important inference rule is the principle of induction ,thatper-
mits proofs by well-founded induction on the ordinal

0 (the logic provides a

constructive definition of the ordinals up to 0 ).
By the principle of definition new function definitions are admitted as axioms
(using defun ) only if its termination is proved by means of an ordinal measure
in which the arguments of each recursive call, if any, decrease. In addition, the
encapsulation principle allows the user to introduce new function symbols (using
encapsulate ) that are constrained to satisfy certain assumptions. To ensure that
the constraints are satisfiable, the user must provide a witness function with the
required properties. Within the scope of an encapsulate , properties stated as
theorems need to be proved for the witnesses; outside, these theorems work as as-
sumed axioms. Together, encapsulation and the derived inference rule, functional
instantiation , provide a second-order aspect [5, 6]: theorems about constrained
functions can be instantiated with function symbols if they are proved to have
the same properties.
The Acl2 theorem prover mechanizes the logic, being particularly well suited
for obtaining automated proofs based on simplification and induction. Although
the prover is automatic in the sense that once a proof attempt is started (with
defthm ) the user can no longer interact, nevertheless it is interactive in a deeper
sense: usually, the role of the user is to lead the prover to a preconceived hand-
proof, by proving a suitable collection of lemmas that are used as rewrite rules
in subsequent proofs (these lemmas are usually discovered by the user after the
inspection of failed proofs). We used this kind of interaction to obtain the formal
proofs presented here. For a detailed description of Acl2, we refer the reader to
the Acl2 book [5].

1 Nevertheless, the degree of automation of the Acl2 theorem prover is higher than
in other systems with more expressive logics.
2 Although we are aware that prefix notation may be inconvenient for people not used
to Lisp, we will maintain it to emphasize the use of a real programming language.