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:
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 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:
We use multisets (by means of the defmul macro) to prove termination of an iterative version of Ackermann's function
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.
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.
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.
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.
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.