BDD-based decision procedures for the modal logic K ★

Journal of Applied Non-Classical Logics 16 (1-2):169-207 (2006)
  Copy   BIBTEX


We describe BDD-based decision procedures for the modal logic K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Instead, we compute certain fixpoints of a set of types — which can be viewed as an on-the-fly emptiness of the automaton. We use BDDs to represent and manipulate such type sets, and investigate different kinds of representations as well as a “level-based” representation scheme. The latter turns out to speed up construction and reduce memory consumption considerably. We also study the effect of formula simplification on our decision procedures. To prove the viability of our approach, we compare our approach with a representative selection of other approaches, including a translation of K to QBF. Our results indicate that the BDD-based approach dominates for modally heavy formulae, while search-based approaches dominate for propositionally heavy formulae.



    Upload a copy of this work     Papers currently archived: 91,271

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Terminating tableau systems for hybrid logic with difference and converse.Mark Kaminski & Gert Smolka - 2009 - Journal of Logic, Language and Information 18 (4):437-464.
Four simple systems of modal propositional logic.Gerald J. Massey - 1965 - Philosophy of Science 32 (3/4):342-355.
Decision procedures for some strong hybrid logics.Andrzej Indrzejczak & Michał Zawidzki - 2013 - Logic and Logical Philosophy 22 (4):389-409.
Decision procedures for Lewis system S1 and related modal systems.Anjan Shukla - 1970 - Notre Dame Journal of Formal Logic 11 (2):141-180.
Displaying the modal logic of consistency.Heinrich Wansing - 1999 - Journal of Symbolic Logic 64 (4):1573-1590.
Some Connections between Topological and Modal Logic.Kurt Engesser - 1995 - Mathematical Logic Quarterly 41 (1):49-64.


Added to PP

59 (#263,790)

6 months
7 (#382,198)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Modal Logic: Graph. Darst.Patrick Blackburn, Maarten de Rijke & Yde Venema - 2001 - New York: Cambridge University Press. Edited by Maarten de Rijke & Yde Venema.
Some philosophical problems from the standpoint of artificial intelligence.John McCarthy & Patrick Hayes - 1969 - In B. Meltzer & Donald Michie (eds.), Machine Intelligence 4. Edinburgh University Press. pp. 463--502.

View all 6 references / Add more references