EXPTIME tableaux for ALC using sound global caching
Date
2007
Authors
Gore, Rajeev
Nguyen, Linh Anh
Journal Title
Journal ISSN
Volume Title
Publisher
Bozen-Bolzano University Press
Abstract
We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a different branch of the tableau, thereby building global caching into the algorithm from the start. Doing so is important since it allows us to reason explicitly about the correctness of global caching. We then show that propagating both satisfiability and unsatisfiability via the and-or structure of the graph remains sound. In the longer paper, by combining global caching, propagation and cutoffs, our framework reduces the search space more significantly than the framework of [1]. Also, the freedom to use arbitrary search heuristics significantly increases its application potential. A longer version with all optimisations is currently under review for a journal. An extension for SHI will appear in TABLEAUX 2007.
Description
Keywords
Keywords: Decision procedure; Description logic; Optimal complexity; Optimisations; Satisfiability; Search heuristics; Search spaces; Formal languages; Formal logic; Heuristic algorithms; Optimization; Data description Decision procedures; Optimal complexity; Sound caching
Citation
Collections
Source
2007 International Workshop on Description Logics Proceedings
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
DOI
Restricted until
2037-12-31
Downloads
File
Description