A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover
No abstract available.
Related papers
- Theorem Proving Using Lazy Proof Explication CAV 2003
- A proof-theoretic approach to certifying skolemization CPP 2019
- A Lightweight Formalization of the Metatheory of Bisimulation-Up-To CPP 2015
- Improved Assistance for Interactive Proof (Keynote) CPP 2023
- ALASCA: Reasoning in Quantified Linear Arithmetic TACAS 2023
- A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq Haskell 2017
- Dependent types ensure partial correctness of theorem provers JFP 2004
- Reasoning About Programs POPL 1973