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

DOI10.1007/978-3-319-08587-6_19zbMATH Open1423.68417OpenAlexW2554014980MaRDI QIDQ3192197FDOQ3192197

Rajeev Goré, Jesse Wu, Jimmy Thomson

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

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

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• IntHistGC
• Efficient SAT-based proof search in intuitionistic propositional logic
• SAT-based proof search in intermediate propositional logics
• A tableaux calculus for default intuitionistic logic

Uses Software

• ILTP
• fCube

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)