EXPtime tableaux for ALC
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.
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- Table algebras
- scientific article; zbMATH DE number 749695
- Complementary algorithms for tableaux
- The structure of alternative tableaux
- The excedance algebra
- Algebraic composition of function tables
- Extending (nonclassical) table algebra
- A description logic with transitive and inverse roles and role hierarchies
- A guide to completeness and complexity for modal logics of knowledge and belief
- A modal perspective on the computational complexity of attribute value grammar
- A new method for bounding the complexity of modal logics
- A practical decision method for propositional dynamic logic (preliminary report)
- A proper hierarchy of propositional sequent calculi
- A PSpace algorithm for graded modal logic
- An empirical analysis of modal theorem provers
- Attributive concept descriptions with complements
- Automata-theoretic techniques for modal logics of programs
- Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
- Computational complexity of terminological reasoning in BACK
- Decidability by resolution for propositional modal logics
- Efficient loop-check for backward proof search in some non-classical propositional logics
- EXPtime tableaux for ALC
- Foundations of a functional approach to knowledge representation
- Hintikka multiplicities in matrix decision methods for some propositional modal logics
- scientific article; zbMATH DE number 1612538 (Why is no real title available?)
- scientific article; zbMATH DE number 1612540 (Why is no real title available?)
- scientific article; zbMATH DE number 1612554 (Why is no real title available?)
- scientific article; zbMATH DE number 1612595 (Why is no real title available?)
- scientific article; zbMATH DE number 1614703 (Why is no real title available?)
- scientific article; zbMATH DE number 3986613 (Why is no real title available?)
- scientific article; zbMATH DE number 67502 (Why is no real title available?)
- scientific article; zbMATH DE number 67503 (Why is no real title available?)
- scientific article; zbMATH DE number 1267561 (Why is no real title available?)
- scientific article; zbMATH DE number 534879 (Why is no real title available?)
- scientific article; zbMATH DE number 1142324 (Why is no real title available?)
- scientific article; zbMATH DE number 1149405 (Why is no real title available?)
- scientific article; zbMATH DE number 1149436 (Why is no real title available?)
- scientific article; zbMATH DE number 1149440 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 1435945 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- Hyper tableaux
- On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the Region Connection Calculus
- Optimizing description logic subsumption
- Practical reasoning for very expressive description logics
- Proof methods for modal and intuitionistic logics
- Propositional dynamic logic of regular programs
- Reasoning about infinite computations
- Reasoning about temporal relations
- SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Simplification: A general constraint propagation technique for propositional and modal tableaux
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- Strongly analytic tableaux for normal modal logics
- Tableau methods for formal verification of multi-agent distributed systems
- Tableau methods for modal and temporal logics
- The complexity of concept languages
- The Complexity of Propositional Proofs
- The Computational Complexity of Provability in Systems of Modal Propositional Logic
- Translation Methods for Non-Classical Logics: An Overview
- Uniform and non uniform strategies for tableaux calculi for modal logics
- Uniform Gentzen systems
- Unique Binary-Search-Tree Representations and Equality Testing of Sets and Sequences
- On the scalability of description logic instance retrieval
- On the complexities of consistency checking for restricted UML class diagrams
- EXPtime tableaux for ALC
- Optimised exptime tableaux for \(\mathcal{SHJN}\) over finite residuated lattices
- ExpTime tableaux with global caching for hybrid PDL
- A prover dealing with nominals, binders, transitivity and relation hierarchies
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Tractable approximate deduction for OWL
- Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
- Generalized satisfiability for the description logic \(\mathcal{ALC}\) (extended abstract)
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- PS\textsc{pace} tableau algorithms for acyclic modalized \({\mathcal{ALC}}\)
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description)
- Description Logics
- Improvement of a tableau-based algorithm and the finite-step halting theorem
- Generalized satisfiability for the description logic \(\mathcal{ALC}\)
- A Tableau Calculus for Temporal Description Logic: the Expanding Domain Case
- Hybrid tableaux for the difference modality
- A Tableau Calculus for Regular Grammar Logics with Converse
- Probabilistic reasoning in the description logic \(\mathcal {ALCP}\) with the principle of maximum entropy
- Global caching for coalgebraic description logics
- Optimized description logic reasoning via core blocking
- The Probabilistic Description Logic
- Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\)
- Complexity of hybrid logics over transitive frames
- ExpTime tableau decision procedures for regular grammar logics with converse
- Deciding expressive description logics in the framework of resolution
This page was built for publication: EXPtime tableaux for ALC
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1589576)
