EXPTIME tableaux for ALC

F.M. Donini, F. Massacci

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

The last years have seen two major advances in Knowledge Representation and Reasoning. First, many interesting problems (ranging from Semi-structured Data to Linguistics) were shown to be expressible in logics whose main deductive problems are EXPTIME-complete. Second, experiments in automated reasoning have substantially broadened the meaning of `practical tractability'. Instances of realistic size for PSPACE-complete problems are now within reach for implemented systems. Still, there is a gap between the reasoning services needed by the expressive logics mentioned above and those provided by the current systems. Indeed, the algorithms based on tree-automata, which are used to prove EXPTIME-completeness, require exponential time and space even in simple cases. On the other hand, current algorithms based on tableau methods can take advantage of such cases, but require double exponential time in the worst case. We propose a tableau calculus for the description logic ALC for checking the satisfiability of a concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based decision procedure working in single exponential time. To guarantee the ease of implementation, we also discuss the effects that optimizations (propositional backjumping, simplification, semantic branching, etc.) might have on our complexity result, and introduce a few optimizations ourselves.
Original languageEnglish
Pages (from-to)87-138
JournalArtificial Intelligence
Volume124
Issue number1
DOIs
Publication statusPublished - 2000
Externally publishedYes

Fingerprint

Dive into the research topics of 'EXPTIME tableaux for ALC'. Together they form a unique fingerprint.

Cite this