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

  • William McCune
  • Olga Shumsky
Part of the Advances in Formal Methods book series (ADFM, volume 4)


This case study shows how non-ACL2 programs can be combined with ACL2 functions in such a way that useful properties can be proved about the composite programs. Nothing is proved about the non-ACL2 programs Instead, the results of the non-ACL2 programs are checked at run time by ACL2 functions, and properties of these checker functions are proved. The application is resolution/paramodulation automated theorem proving for first-order logic. The top ACL2 function takes a conjecture, preprocesses the conjecture, and calls a non-ACL2 program to search for a proof or countermodel. If the non-ACL2 program succeeds, ACL2 functions check the proof or countermodel. The top ACL2 function is proved sound with respect to finite interpretations.


Conjunctive Normal Form Universal Closure Proof Procedure Conjunctive Normal Form Formula Proof Checker 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • William McCune
    • 1
  • Olga Shumsky
    • 2
  1. 1.Mathematics and Computer Science DivisionArgonne National LaboratoryArgonneUSA
  2. 2.Department of Electrical and Computer EngineeringNorthwestern UniversityEvanstonUSA

Personalised recommendations