[ US ] [ CCIA ] [ Teaching ] [ SLC ] [e-mail]
Multiset relations: a tool for proving termination (in ACL2)

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.lisp

Definition 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.

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