*
Computational Logic
Group, CCIA, Universidad de Sevilla, Spain *

Here are the books we developed to implement well-founded multiset extension of a given well-founded ACL2 relation.

**
The main books:
**

*Main theorem and useful lemmas: multiset.lisp*This book contains an ACL2 proof of the following theorem: "Given a well-founded relation

*rel*, the relation induced by*rel*on multisets is also well-founded".This book also contains some useful rules to deal with multisets.*Definition of*__defmul__: defmul.lispDefinition of the

*defmul*macro, a tool for defining well-founded multiset relations in a convenient way. An auxiliary macro*defmul-components*is also defined. The book*multiset.lisp*is included.

**
Examples using defmul:
**

*A tail-recursive version of Ackermann's function: ackermann.lisp*We use multisets (by means of the

*defmul*macro) to prove termination of an iterative version of Ackermann's function*An iterative version of McCarthy's 91 function: mccarthy-91.lisp*A multiset ordering is defined using

*defmul*as a tool for proving termination of an iterative version of McCarthy's 91 function. Some additional properties are also proved.*A tail-recursive version of a general binary recursive algorithm: binrec.lisp*We use

*defmul*to obtain a well-founded relation needed for tha admission of tail-recursive version of a geneal binary recursion scheme. We also prove the equivalence of both recursive schemes.*A generic SAT prover*:Following the above link, an application of ACL2 to reason about SAT provers can be found. In particular

*defmul*is used in the admission of a generic transformation-based SAT prover.*Newman's lemma: abstract-proofs.lisp, confluence.lisp, newman.lisp and convergent.lisp*A mechanical proof of Newman's lemma and some corollaries of this important result about abstract reduction relations.

*Defmul*is used in the book*newman.lisp*, the rest of the books are needed to show decidability of equivalence relations described by a terminating and locally confluent reduction relations. This example is part of a larger work done by this group, an attempt to formalize equational reasoning in ACL2.

**All the books (except those of the SAT example) are tared and gziped in acl2-mul.tgz.****To certify all the books, see the README file.****A paper:**Multiset relations: a tool for proving termination, presented at ACL2 Workshop 2000. See also the slides.

Dpto. de Ciencias de la Computación e Inteligencia Artificial

Facultad de Informática y Estadística

Universidad de Sevilla