Deciding expressive description logics in the framework of resolution
From MaRDI portal
Recommendations
Cites work
- A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes
- A principle for incorporating axioms into the first-order translation of modal formulae.
- A structure-preserving clause form translation
- Automated Reasoning
- Basic paramodulation
- Combining superposition, sorts and splitting
- Complexity of the two-variable fragment with counting quantifiers
- Complexity Results for First-Order Two-Variable Logic with Counting
- Computing small clause normal forms
- EXPtime tableaux for ALC
- scientific article; zbMATH DE number 1614714 (Why is no real title available?)
- scientific article; zbMATH DE number 440110 (Why is no real title available?)
- scientific article; zbMATH DE number 67503 (Why is no real title available?)
- scientific article; zbMATH DE number 1303345 (Why is no real title available?)
- scientific article; zbMATH DE number 1348742 (Why is no real title available?)
- scientific article; zbMATH DE number 1936671 (Why is no real title available?)
- scientific article; zbMATH DE number 1507191 (Why is no real title available?)
- scientific article; zbMATH DE number 1765711 (Why is no real title available?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Loosely guarded fragment of first-order logic has the finite model property
- Modal languages and bounded fragments of predicate logic
- Normal form transformations
- On the efficiency of subsumption algorithms
- Ordered chaining calculi for first-order theories of transitive relations
- Practical reasoning for very expressive description logics
- Propositional dynamic logic of regular programs
- Resolution methods for the decision problem
- Resolution Strategies as Decision Procedures
- Resolution theorem proving
- Resolution-based methods for modal logics
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Rewriting
- Splitting through new proposition symbols
- Theorem proving with ordering and equality constrained clauses
Cited in
(22)- Deciding inseparability and conservative extensions in the description logic
- Tableau reasoning for description logics and its extension to probabilities
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- A tableau decision procedure for \(\mathcal{SHOIQ}\)
- scientific article; zbMATH DE number 1614719 (Why is no real title available?)
- Type-elimination-based reasoning for the description logic \(\mathcal {SHIQ}b_s\) using decision diagrams and disjunctive Datalog
- A decidable quantified fragment of set theory involving ordered pairs with applications to description logics
- A resolution based description logic calculus
- scientific article; zbMATH DE number 1507191 (Why is no real title available?)
- Harald Ganzinger's legacy: contributions to logics and programming
- First-order resolution methods for modal logics
- A Decidable Constructive Description Logic
- Probabilistic DL reasoning with pinpointing formulas: a Prolog-based approach
- The data complexity of ontology-mediated queries with closed predicates
- On the finite controllability of conjunctive query answering in databases under open-world assumption
- Prolog Based Description Logic Reasoning
- Logic for Programming, Artificial Intelligence, and Reasoning
- Semantic web
- Top-\(k\) retrieval for ontology mediated access to relational databases
- Decidability of SHIQ with complex role inclusion axioms
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Incremental classification of description logics ontologies
This page was built for publication: Deciding expressive description logics in the framework of resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q924723)
