Using BDDs for non-classical propositional theorem proving

Abstract

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 cases we present the reasoning behind the decision procedure to best illustrate how the component ideas can be re-arranged and combined together to produce decision procedures for other logics. The BDD approach we describe constructs a finite model which contains a proxy for every world which appears in any model, and represents this finite set of proxy worlds using a BDD. Any Kripke-relations in the finite model are also represented as sets of pairs using BDDs. The semantics of the particular logic direct a refinement process which either starts with all potential worlds and removes worlds which do not appear in any model to find a greatest-fixpoint, or starts with no worlds and adds worlds which appear in some model to find a least-fixpoint. Once the final model is found, satisfiability and validity of a formula P is reduced to determining whether any worlds in the particular model satisfy or falsify P. We can also answer questions of global logical consequence by restricting the worlds considered to those satisfying a set of global assumptions. Because the method constructs models, or pseudo-models which can be converted into models, whenever the decision procedure determines a formula to be (counter)-satisfiable, a (counter)-model can be extracted. Validity or unsatisfiabilty on the other hand is determined by the lack of a model, but we also show how to extract sequent proofs of validity for Bi-Intuitionistic Tense Logic. We also compare implementations of our method for Intuitionistic Logic and Computation Tree Logic against other state of the art theorem provers and find that with appropriate optimisations the decision procedures are competitive. In particular we apply algorithmic optimisations such as early termination or converting a question of validity to a question of global logical consequence and pre-processing techniques such as rewriting formulae to reduce the size of the closure. We also consider implementation concerns such as the order to construct intermediate BDDs to minimise size, as well as the impact of different BDD variable orders.