An improved BDD method for intuitionistic propositional logic: BDDIntKt system description

DOI10.1007/978-3-642-38574-2_19MaRDI QIDQ4928444zbMATH OpenOpenAlexFDO

Authors Rajeev Goré, Jimmy Thomson

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38574-2_19

Mathematics Subject Classification ID

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

Recommendations

• BDD-based automated reasoning for propositional bi-intuitionistic tense logics
• Binary decision diagrams for first-order predicate logic.
• Optimization techniques for propositional intuitionistic logic and their implementation
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• SAT modulo intuitionistic implications

Cited in

(5)

• BDD-based automated reasoning for propositional bi-intuitionistic tense logics
• BDDIntKt
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• scientific article; zbMATH DE number 2090285 (Why is no real title available?)
• Improved decision procedures for multi-modal tense logic using CEGAR-tableaux

Describes a project that uses

Uses Software

• ILTP
• BuDDy
• Imogen
• fCube

This page was built for publication: An improved BDD method for intuitionistic propositional logic: BDDIntKt system description

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