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 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