A resolution theorem prover for intuitionistic logic

DOI10.1007/3-540-61511-3_65zbMath1412.68265OpenAlexW1787768633MaRDI QIDQ4647496

Tanel Tammet

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

zbMATH Keywords

sequent calculusintuitionistic logicproof searchresolution methoddecidable class

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20)

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

• PRIZ

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