A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description

DOI10.1007/978-3-319-08587-6_19MaRDI QIDQ3192197zbMATH OpenOpenAlexFDO

Authors Rajeev Goré, Jimmy Thomson, Jesse Wu

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_19

Mathematics Subject Classification ID

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

Recommendations

• An Intuitionistic Predicate Logic Theorem Prover
• Theorem prover for intuitionistic logic based on the inverse method
• fCube: an efficient prover for intuitionistic propositional logic
• A resolution theorem prover for intuitionistic logic
• Optimization techniques for propositional intuitionistic logic and their implementation

Cited in

(8)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• General clauses for SAT-based proof search in intuitionistic propositional logic
• Intuitionistic Decision Procedures Since Gentzen
• IntHistGC
• scientific article; zbMATH DE number 1770113 (Why is no real title available?)
• Efficient SAT-based proof search in intuitionistic propositional logic
• SAT-based proof search in intermediate propositional logics
• A tableaux calculus for default intuitionistic logic

Describes a project that uses

Uses Software

• fCube
• ILTP

This page was built for publication: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192197)