TY - GEN
T1 - BDD-based automated reasoning for propositional Bi-intuitionistic tense logics
AU - Goré, Rajeev
AU - Thomson, Jimmy
PY - 2012
Y1 - 2012
N2 - We give Binary Decision Diagram (BDD) based methods for deciding validity and satisfiability of propositional Intuitionistic Logic Int and Bi-intuitionistic Tense Logic BiKt. We handle intuitionistic implication and bi-intuitionistic exclusion by treating them as modalities, but the move to an intuitionistic basis requires careful analysis for handling the reflexivity, transitivity and antisymmetry of the underlying Kripke relation. BiKt requires a further extension to handle the interactions between the intuitionistic and modal binary relations, and their converses. We explain our methodology for using the Kripke semantics of these logics to constrain the underlying least and greatest fixpoint approaches of the finite model construction. With some optimisations this technique is competitive with the state of the art theorem provers for Intuitionistic Logic using the ILTP benchmark and randomly generated formulae.
AB - We give Binary Decision Diagram (BDD) based methods for deciding validity and satisfiability of propositional Intuitionistic Logic Int and Bi-intuitionistic Tense Logic BiKt. We handle intuitionistic implication and bi-intuitionistic exclusion by treating them as modalities, but the move to an intuitionistic basis requires careful analysis for handling the reflexivity, transitivity and antisymmetry of the underlying Kripke relation. BiKt requires a further extension to handle the interactions between the intuitionistic and modal binary relations, and their converses. We explain our methodology for using the Kripke semantics of these logics to constrain the underlying least and greatest fixpoint approaches of the finite model construction. With some optimisations this technique is competitive with the state of the art theorem provers for Intuitionistic Logic using the ILTP benchmark and randomly generated formulae.
UR - http://www.scopus.com/inward/record.url?scp=84863634895&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-31365-3_24
DO - 10.1007/978-3-642-31365-3_24
M3 - Conference contribution
SN - 9783642313646
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 301
EP - 315
BT - Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Proceedings
T2 - 6th International Joint Conference on Automated Reasoning, IJCAR 2012
Y2 - 26 June 2012 through 29 June 2012
ER -