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.

References in zbMATH (referenced in 25 articles , 1 standard article )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Frumkin, Asya; Feldman, Yotam M.Y.; Lhoták, Ondřej; Padon, Oded; Sagiv, Mooly; Shoham, Sharon: Property directed reachability for proving absence of concurrent modification errors (2017)
  2. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  3. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  4. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  5. Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through herbrand’s theorem (2013)
  6. Kaliszyk, Cezary; Urban, Josef: Proch: proof reconstruction for HOL light (2013)
  7. Wiedijk, Freek: Pollack-inconsistency (2012)
  8. Araújo, João; McCune, William: Computer solutions of problems in inverse semigroups. (2010)
  9. Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik: Integrating external deduction tools with ACL2 (2009)
  10. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  11. Urban, Josef; Sutcliffe, Geoff: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (2008)
  12. Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
  13. Urban, Josef; Sutcliffe, Geoff: ATP cross-verification of the Mizar MPTP challenge problems (2007)
  14. Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Van Gelder, Allen: Using the TPTP language for writing derivations and finite interpretations (2006)
  15. de Nivelle, Hans: Translation of resolution proofs into short first-order proofs without choice axioms (2005)
  16. Denney, Ewen; Fischer, Bernd; Schumann, Johann: Using automated theorem provers to certify auto-generated aerospace software (2004)
  17. de Nivelle, Hans: Translation of resolution proofs into short first-order proofs without choice axioms. (2003)
  18. Bezem, Marc; Hendriks, Dimitri; de Nivelle, Hans: Automated proof construction in type theory using resolution (2002)
  19. de Nivelle, Hans: Extraction of proofs from the clausal normal form transformation (2002)
  20. Ruiz-Reina, José-Luis; Alonso, José-Antonio; Hidalgo, María-José; Martín-Mateos, Francisco-Jesús: Formal proofs about rewriting using ACL2 (2002)

1 2 next