Using BDDs for non-classical propositional theorem proving
This thesis investigates a method for determining satisfiability and validity using Binary Decision Diagrams (BDDs) to construct finite (pseudo-)models. The method was originally considered by Pan et al and Marrero. We extend the method to deal with a wide variety of non-classical propositional logics including the 15 basic normal modal logics, multimodal logics, tense logic, intuitionistic logic, bi-intuitionistic tense logic, linear time logic, and propositional dynamic logic. In all of these...[Show more]
|Collections||Open Access Theses|
|b36002239_Thomson_Jimmy.pdf||322.13 MB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.