Skip navigation
Skip navigation

Using BDDs for non-classical propositional theorem proving

Thomson, James Robert

Description

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)
URI: http://hdl.handle.net/1885/155911
DOI: 10.25911/5d514d3b6dacc

Download

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:  22 January 2019/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator