BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|01_Gore_BDD-Based_Automated_Reasoning_2012.pdf||193.43 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.