Theorem Proving Using Lazy Proof Explication
No abstract available.
Related papers
- A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover TACAS 2005
- The adequacy of Launchbury's natural semantics for lazy evaluation JFP 2018
- Reasoning About Programs POPL 1973
- PureCake: A Verified Compiler for a Lazy Functional Language PLDI 2023
- A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic CPP 2024
- Call-by-value and call-by-name: A simple proof of a classic theorem JFP 2025
- Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 TACAS 2025
- BliStrTune: hierarchical invention of theorem proving strategies CPP 2017