Skip navigation
Skip navigation
Open Research will be down for maintenance between 8:00 and 8:15 am on Tuesday, December 1 2020.

Using BDDs for non-classical propositional theorem proving

Thomson, James Robert


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]

CollectionsOpen Access Theses
Date published: 2014
Type: Thesis (PhD)
DOI: 10.25911/5d514d3b6dacc


File Description SizeFormat Image
b36002239_Thomson_Jimmy.pdf322.13 MBAdobe PDFThumbnail

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