Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
McCune, W., Shumsky, O. (2000). Ivy: A Preprocessor and Proof Checker for First-Order Logic. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds) Computer-Aided Reasoning. Advances in Formal Methods, vol 4. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3188-0_16
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3188-0_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4981-3
Online ISBN: 978-1-4757-3188-0
eBook Packages: Springer Book Archive