Skip navigation
Skip navigation

BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics

Gore, Rajeev; Thomson, James


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]

CollectionsANU Research Publications
Date published: 2012
Type: Conference paper
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-642-31365-3_24


File Description SizeFormat Image
01_Gore_BDD-Based_Automated_Reasoning_2012.pdf193.43 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator