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 39 articles , 1 standard article )

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

1 2 next

  1. Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca: Universal invariant checking of parametric systems with quantifier-free SMT reasoning (2021)
  2. Padon, Oded; Hoenicke, Jochen; McMillan, Kenneth L.; Podelski, Andreas; Sagiv, Mooly; Shoham, Sharon: Temporal prophecy for proving temporal properties of infinite-state systems (2021)
  3. Peyras, Quentin; Brunel, Julien; Chemouil, David: A decidable and expressive fragment of Many-Sorted first-order linear temporal logic (2021)
  4. Voigt, Marco: Decidable (\exists^*\forall^*) first-order fragments of linear rational arithmetic with uninterpreted predicates (2021)
  5. Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav: Learning inductive invariants by sampling from frequency distributions (2020)
  6. Kragl, Bernhard; Qadeer, Shaz; Henzinger, Thomas A.: Synchronizing the asynchronous (2018)
  7. Madhusudan, P.; Mathur, Umang; Saha, Shambwaditya; Viswanathan, Mahesh: A decidable fragment of second order logic with applications to synthesis (2018)
  8. Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon: Bounded quantifier instantiation for checking inductive invariants (2017)
  9. 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)
  10. Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef: (\textPara^2): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms (2017)
  11. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  12. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  13. Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
  14. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  15. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  16. C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel Paleo: PROOFTOOL: a GUI for the GAPT Framework (2013) arXiv
  17. Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through Herbrand’s theorem (2013)
  18. Kaliszyk, Cezary; Urban, Josef: PRocH: proof reconstruction for HOL Light (2013)
  19. Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph: More SPASS with Isabelle. Superposition with hard sorts and configurable simplification (2012)
  20. Wiedijk, Freek: Pollack-inconsistency (2012)

1 2 next