EXPtime tableaux for ALC
From MaRDI portal
Publication:1589576
DOI10.1016/S0004-3702(00)00070-9zbMath0952.68136OpenAlexW2337512840WikidataQ58006968 ScholiaQ58006968MaRDI QIDQ1589576
Fabio Massacci, Francesco M. Donini
Publication date: 12 December 2000
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0004-3702(00)00070-9
Related Items
Tractable approximate deduction for OWL ⋮ ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching ⋮ Generalized satisfiability for the description logic \(\mathcal{ALC}\) ⋮ The Probabilistic Description Logic ⋮ Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\) ⋮ Complexity of hybrid logics over transitive frames ⋮ Deciding expressive description logics in the framework of resolution ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description) ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Generalized Satisfiability for the Description Logic $\mathcal{ALC}$ ⋮ Global Caching for Coalgebraic Description Logics ⋮ Optimized Description Logic Reasoning via Core Blocking ⋮ A Tableau Calculus for Regular Grammar Logics with Converse ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ Description Logics ⋮ Hybrid Tableaux for the Difference Modality ⋮ ExpTime tableau decision procedures for regular grammar logics with converse ⋮ On the scalability of description logic instance retrieval ⋮ On the complexities of consistency checking for restricted UML class diagrams ⋮ EXPtime tableaux for ALC ⋮ Probabilistic Reasoning in the Description Logic $$\mathcal {ALCP}$$ with the Principle of Maximum Entropy
Uses Software
Cites Work
- Attributive concept descriptions with complements
- Foundations of a functional approach to knowledge representation
- Proof methods for modal and intuitionistic logics
- Automata-theoretic techniques for modal logics of programs
- Computational complexity of terminological reasoning in BACK
- A guide to completeness and complexity for modal logics of knowledge and belief
- Propositional dynamic logic of regular programs
- Decidability by resolution for propositional modal logics
- On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the Region Connection Calculus
- A modal perspective on the computational complexity of attribute value grammar
- Reasoning about infinite computations
- A proper hierarchy of propositional sequent calculi
- The complexity of concept languages
- EXPtime tableaux for ALC
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- The Computational Complexity of Provability in Systems of Modal Propositional Logic
- Tableau methods for formal verification of multi-agent distributed systems
- Optimizing description logic subsumption
- A description logic with transitive and inverse roles and role hierarchies
- Unique Binary-Search-Tree Representations and Equality Testing of Sets and Sequences
- Translation Methods for Non-Classical Logics: An Overview
- Reasoning about temporal relations
- SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
- An empirical analysis of modal theorem provers
- Practical reasoning for very expressive description logics
- Hintikka multiplicities in matrix decision methods for some propositional modal logics
- Efficient loop-check for backward proof search in some non-classical propositional logics
- Building decision procedures for modal logics from propositional decision procedures — The case study of modal K
- Uniform and non uniform strategies for tableaux calculi for modal logics
- The Complexity of Propositional Proofs
- Strongly analytic tableaux for normal modal logics
- Hyper tableaux
- A practical decision method for propositional dynamic logic (Preliminary Report)
- Uniform Gentzen systems
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
