ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
arXiv:1205.5838
Abstract
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIQ when numbers are coded in unary. Our procedure is based on global state caching and integer linear feasibility checking.
References in corpus (4)
- Complexity Results and Practical Algorithms for Logics in Knowledge Representation
- Reasoning with Individuals for the Description Logic SHIQ
- Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
- A Cut-Free ExpTime Tableau Decision Procedure for the Logic Extending Converse-PDL with Regular Inclusion Axioms