A resolution-based decision procedure for SHOIQ.

Cites Work

A structure-preserving clause form translation
Resolution theorem proving
Title not available (Why is that?)
Title not available (Why is that?)
A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
Term Rewriting and All That
Resolution decision procedures
Combining superposition, sorts and splitting
Rewrite-based Equational Theorem Proving with Selection and Simplification
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Complexity of the two-variable fragment with counting quantifiers
Theorem proving with ordering and equality constrained clauses
Basic paramodulation
PSpace reasoning for graded modal logics
Paramodulation-based theorem proving
Title not available (Why is that?)
The intractability of resolution
Logic for Programming, Artificial Intelligence, and Reasoning
Title not available (Why is that?)
A tableau decision procedure for $\mathcal{SHOIQ}$
Title not available (Why is that?)
Resolution Strategies as Decision Procedures
Resolution-based methods for modal logics
Title not available (Why is that?)
Complexity Results for First-Order Two-Variable Logic with Counting
Title not available (Why is that?)
Automated Deduction – CADE-19
Resolution methods for the decision problem
On the decidability of the PVD class with equality
Title not available (Why is that?)
Deciding the guarded fragments by resolution
Semantic integration of heterogeneous information sources
Deciding the $E^+$-class by an a posteriori, liftable order
A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$
Title not available (Why is that?)
Title not available (Why is that?)
Automated Reasoning

Cited In (8)

Title not available (Why is that?)
ABox abduction in the description logic $\mathcal{ALC}$
Data complexity of query answering in expressive description logics via tableaux
A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$
First-Order Resolution Methods for Modal Logics
Resolution with order and selection for hybrid logics
Algebraic tableau reasoning for the description logic $\mathcal{SHOQ}$
Harald Ganzinger’s Legacy: Contributions to Logics and Programming

   Recommendations

A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$ 👍 👎
A tableau decision procedure for $\mathcal{SHOIQ}$ 👍 👎
Deciding expressive description logics in the framework of resolution 👍 👎
Logic for Programming, Artificial Intelligence, and Reasoning 👍 👎
Title not available (Why is that?) 👍 👎

This page was built for publication: A resolution-based decision procedure for ${\mathcal{SHOIQ}}$.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q928657)