A resolution theorem prover for intuitionistic logic
From MaRDI portal
Publication:4647496
DOI10.1007/3-540-61511-3_65zbMath1412.68265OpenAlexW1787768633MaRDI QIDQ4647496
Publication date: 15 January 2019
Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61511-3_65
Related Items
Two loop detection mechanisms: A comparison ⋮ ileanTAP: An intuitionistic theorem prover ⋮ Theorem prover for intuitionistic logic based on the inverse method ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ Proof-search in type-theoretic languages: An introduction ⋮ A uniform procedure for converting matrix proofs into sequent-style systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Resolution methods for the decision problem
- Proof strategies in linear logic
- The axioms of constructive geometry
- The PRIZ system and propositional calculus
- Contraction-free sequent calculi for intuitionistic logic
- Some applications of Gentzen's proof theory in automated deduction
- An Intuitionistic Predicate Logic Theorem Prover
- A Machine-Oriented Logic Based on the Resolution Principle