Ivy: A Preprocessor and Proof Checker for First-order Logic

William McCune and Olga Shumsky Matlin

Ivy is a preprocessor and proof checker for resolution/paramodulation theorem provers. It is coded in ACL2 and proved sound for finite interpretations.

Our Chapter of the ACL2 Case Studies Book

Ivy is described in a chapter of Computer-Aided Reasoning: ACL2 Case Studies published by Kluwer Academic. See the Kluwer web page for information on ordering the book.

Where is Ivy?

This information is probably obsolete.

Ivy is distributed with ACL2, in the directory books/workshops/1999/ivy. Check the main ACL2 page for information on how to obtain and intall ACL2 and the separate workshop file. Or, obtain a separate version of Ivy from the ACL2 site here.

Or, you can take the version that we sent to the ACL2 maintainers (April 12, 2000). This contains everything: the Ivy source and theorems (ACL2 books), full distributions of Otter-3.0.6 and MACE-1.3.4, examples, and exercises. (Some of the README files and makefiles are different.)

This works with ACL2-v2.4 and -v2.5. Versions of Ivy obtained from the main ACL2 page may have been changed from the original to make Ivy work with the current release of ACL2. Here is the list of the necessary changes so far.