Ivy
Ivy: A Preprocessor and Proof Checker for First-Order Logic. 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.
Keywords for this software
References in zbMATH (referenced in 21 articles , 1 standard article )
Showing results 1 to 20 of 21.
Sorted by year (- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
- Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through herbrand’s theorem (2013)
- Kaliszyk, Cezary; Urban, Josef: Proch: proof reconstruction for HOL light (2013)
- Wiedijk, Freek: Pollack-inconsistency (2012)
- Araújo, João; McCune, William: Computer solutions of problems in inverse semigroups. (2010)
- Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik: Integrating external deduction tools with ACL2 (2009)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Urban, Josef; Sutcliffe, Geoff: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (2008)
- Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
- Urban, Josef; Sutcliffe, Geoff: ATP cross-verification of the Mizar MPTP challenge problems (2007)
- Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Van Gelder, Allen: Using the TPTP language for writing derivations and finite interpretations (2006)
- de Nivelle, Hans: Translation of resolution proofs into short first-order proofs without choice axioms (2005)
- Denney, Ewen; Fischer, Bernd; Schumann, Johann: Using automated theorem provers to certify auto-generated aerospace software (2004)
- de Nivelle, Hans: Extraction of proofs from the clausal normal form transformation (2002)
- Ruiz-Reina, José-Luis; Alonso, José-Antonio; Hidalgo, María-José; Martín-Mateos, Francisco-Jesús: Formal proofs about rewriting using ACL2 (2002)
- Bittencourt, Guilherme; Tonin, Isabel: A proof strategy based on a dual representation (2001)
- Moore, J.Strother: Rewriting for symbolic execution of state machine models (2001)
- Ruiz-Reina, José-Luis; Alonso, José-Antonio; Hidalgo, María-José; Martín-Mateos, Francisco-Jesús: Formalizing rewriting in the ACL2 theorem prover (2001)