A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
From MaRDI portal
Publication:928657
DOI10.1007/s10817-007-9090-1zbMath1137.68056OpenAlexW2036162877MaRDI QIDQ928657
Publication date: 11 June 2008
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-007-9090-1
Related Items (6)
Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\) ⋮ Resolution with order and selection for hybrid logics ⋮ ABox abduction in the description logic \(\mathcal{ALC}\) ⋮ Data complexity of query answering in expressive description logics via tableaux ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ First-Order Resolution Methods for Modal Logics
Cites Work
- 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
- The intractability of resolution
- A structure-preserving clause form translation
- Resolution methods for the decision problem
- Deciding the \(E^+\)-class by an a posteriori, liftable order
- Deciding the guarded fragments by resolution
- Theorem proving with ordering and equality constrained clauses
- Basic paramodulation
- A tableau decision procedure for \(\mathcal{SHOIQ}\)
- Complexity of the two-variable fragment with counting quantifiers
- PSPACE Reasoning for Graded Modal Logics
- Semantic integration of heterogeneous information sources
- On the decidability of the PVD class with equality
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$
- Resolution Strategies as Decision Procedures
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Resolution-based methods for modal logics
- Term Rewriting and All That
- Complexity Results for First-Order Two-Variable Logic with Counting
- Automated Reasoning
- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
- Logic for Programming, Artificial Intelligence, and Reasoning
- Automated Deduction – CADE-19
This page was built for publication: A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
