There is also web page about this work in our web server.
To certify the books:
1) Check the variables ACL2 and STRUCTURES-BOOK in Makefile, and change them if needed. 2) Then you can execute: make : To certify everything. make multiset : " multiset.lisp and defmul.lisp. make ackermann : " ackermann.lisp. make mccarthy-91 : " mccarthy-91.lisp. make newman : " all the books of Newman's lemma.See the NOTE file for a technical note.
Contents of this directory:
README.html |
this file |
multiset.lisp |
A proof of well-foundedness of the multiset relation induced by a well-founded relation. Also, useful rules for multisets. |
defmul.lisp |
Definition of demul and defmul-components macros. |
examples/ackermann/ackermann.lisp |
Termination of a tail-recursive version of Ackermann's function. |
examples/mccarthy-91/mccarthy-91.lisp |
Termination of an iterative version of McCarthy's 91 function. |
The following books are part of Newman's lemma example: | |
examples/newman/abstract-proofs.lisp |
Basic concepts about abstract reduction relations. |
examples/newman/confluence.lisp |
A decision algorithm of the equivalence relation described by a confluent and normalizing reduction |
examples/newman/newman.lisp |
A proof of Newman's lemma: "Local confluence and termination implies confluence". This book uses defmul. |
examples/newman/local-confluence.lisp |
A decision algorithm for the equivalence relation described by a terminating and locally confluent reduction relation. |