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

Anything in here will be replaced on browsers that support the canvas element

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

Showing results 1 to 20 of 30.
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. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: (\textPara^2): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (2017)
  3. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  4. Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
  5. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  6. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  7. C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo: PROOFTOOL: a GUI for the GAPT Framework (2013) arXiv
  8. Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through Herbrand’s theorem (2013)
  9. Kaliszyk, Cezary; Urban, Josef: PRocH: proof reconstruction for HOL Light (2013)
  10. Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph: More SPASS with Isabelle. Superposition with hard sorts and configurable simplification (2012)
  11. Wiedijk, Freek: Pollack-inconsistency (2012)
  12. Araújo, João; McCune, William: Computer solutions of problems in inverse semigroups. (2010)
  13. Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik: Integrating external deduction tools with ACL2 (2009)
  14. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
  15. Urban, Josef; Sutcliffe, Geoff: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (2008)
  16. Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
  17. Urban, Josef; Sutcliffe, Geoff: ATP cross-verification of the Mizar MPTP challenge problems (2007)
  18. Harrison, John: Towards self-verification of HOL Light (2006)
  19. Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Van Gelder, Allen: Using the \textttTPTPlanguage for writing derivations and finite interpretations (2006)
  20. de Nivelle, Hans: Translation of resolution proofs into short first-order proofs without choice axioms (2005)

1 2 next