A Resolution Procedure for Description Logics with Nominal Schemas

We present a polynomial resolution-based decision procedure for the recently introduced description logic \(\mathcal{ELHOV}_{n}(\sqcap)\) , which features nominal schemas as new language construct. Our algorithm is based on ordered resolution and positive superposition, together with a lifting lemma. In contrast to previous work on resolution for description logics, we have to overcome the fact that \(\mathcal{ELHOV}_{n}(\sqcap)\) does not allow for a normalization resulting in clauses of globally limited size.

Related papers:

title: ELP: Tractable Rules for OWL 2
abstract: We introduce $\text{\sf{ELP}}$ as a decidable fragment of the Semantic Web Rule Language (SWRL) that admits reasoning in polynomial time. $\text{\sf{ELP}}$ is based on the tractable description logic $\mathcal{EL}^{\mathord{+}\mathord{+}}$, and encompasses an extended notion of the recently proposed DL rules for that logic. Thus $\text{\sf{ELP}}$ extends $\mathcal{EL}^{\mathord{+}\mathord{+}}$ with a number of features introduced by the forthcoming OWL 2, such as disjoint roles, local reflexivity, certain range restrictions, and the universal role. We present a reasoning algorithm based on a translation of $\text{\sf{ELP}}$ to Datalog, and this translation also enables the seamless integration of DL-safe rules into $\text{\sf{ELP}}$. While reasoning with DL-safe rules as such is already highly intractable, we show that DL-safe rules based on the Description Logic Programming (DLP) fragment of OWL 2 can be admitted in $\text{\sf{ELP}}$ without losing tractability.

title: Pushing the EL Envelope
abstract: Recently, it has been shown that the small description logic (DL) EL, which allows for conjunction and existential restrictions, has better algorithmic properties than its counterpart FL0, which allows for conjunction and value restrictions. Whereas the subsumption problem in FL0 becomes already intractable in the presence of acyclic TBoxes, it remains tractable in EL even with general concept inclusion axioms (GCIs). On the one hand, we extend the positive result for EL by identifying a set of expressive means that can be added to EL without sacrificing tractability. On the other hand, we show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even EXPTIME-complete. In addition, we show that subsumption in FL0 with GCIs is EXPTIME-complete.

title: Query Answering for OWL-DL with rules
abstract: Both OWL-DL and function-free Horn rules are decidable fragments of first-order logic with interesting, yet orthogonal expressive power. A combination of OWL-DL and rules is desirable for the Semantic Web; however, it might easily lead to the undecidability of interesting reasoning problems. Here, we present a decidable such combination where rules are required to be DL-safe: each variable in the rule is required to occur in a non-DL-atom in the rule body. We discuss the expressive power of such a combination and present an algorithm for query answering in the related logic SHIQ extended with DL-safe rules, based on a reduction to disjunctive programs. sjunctive programs.

title: A better uncle for OWL: nominal schemas for integrating rules and ontologies
abstract: We propose a description-logic style extension of OWL 2 with nominal schemas which can be used like "variable nominal classes" within axioms. This feature allows ontology languages to express arbitrary DL-safe rules (as expressible in SWRL or RIF) in their native syntax. We show that adding nominal schemas to OWL 2 does not increase the worst-case reasoning complexity, and we identify a novel tractable language SROELV3(∩, x) that is versatile enough to capture the lightweight languages OWL EL and OWL RL.

title: Ordered Chaining for Total Orderings
abstract: We design new inference systems for total orderings by applying rewrite techniques to chaining calculi. Equality relations may either be specified axiomatically or built into the deductive calculus via paramodulation or superposition. We demonstrate that our inference systems are compatible with a concept of (global) redundancy for clauses and inferences that covers such widely used simplification techniques as tautology deletion, subsumption, and demodulation. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. Syntactic ordering restrictions on terms and the rewrite techniques which account for their completeness considerably restrict variable chaining. We show that variable elimination is an admissible simplification technique within our redundancy framework, and that consequently for dense total orderings without endpoints no variable chaining is needed at all.

title: Cheap Boolean Role Constructors for Description Logics
abstract: We investigate the possibility of incorporating Boolean role constructors on simple roles into some of today's most popular description logics, focussing on cases where those extensions do not increase complexity of reasoning. We show that the expressive DLs $\mathcal{SHOIQ}$ and $\mathcal{SROIQ}$, serving as the logical underpinning of OWL and the forthcoming OWL 2, can accommodate arbitrary Boolean expressions. The prominent OWL-fragment $\mathcal{SHIQ}$ can be safely extended by safe role expressions, and the tractable fragments $\mathcal{EL}^{++}$ and DLP retain tractability if extended by conjunction on roles, where in the case of DLP the restriction on role simplicity can even be discarded.

title: Reconciling OWL and Rules
abstract: We report on a recent advance in integrating Rules and OWL. We discuss a recent proposal, known as nominal schemas, which realizes a seamless integration of Datalog rules into the description logic SROIQ which underlies OWL 2 DL. We present extensions of the standardized OWL syntaxes to incorporate nominal schemas, reasoning algorithms, and a first naive implementation. And we argue why this approach goes a long way towards overcoming the present paradigm split.

title: Answer Set Programming with Constraints Using Lazy Grounding
abstract: The paper describes a novel methodology to compute stable models in Answer Set Programming. The proposed approach relies on a bottom-up computation that does not require a preliminary grounding phase. The implementation of the framework can be completely realized within the framework of Constraint Logic Programming over finite domains. The use of a high level language for the implementation and the clean structure of the computation offer an ideal framework for the implementation of extensions of Answer Set Programming. In this work, we demonstrate how non-ground arithmetic constraints can be easily introduced in the computation model. The paper provides preliminary experimental results which confirm the potential for this approach.

title: A Tableau Algorithm for Description Logics with Nominal Schema
abstract: Nominalschema is an expressive description logic (DL) construct that was proposed in recent efforts to integrate DLs and (logic programming) rule-based paradigms for the Semantic Web  represented by two "diverging" W3C standards: the DL-based Web Ontology Language (OWL)  whose major variant, OWL 2 DL, is based on the description logic (DL) ${\mathcal{SROIQ}}$ ; and the rulebased Rule Interchange Format (RIF) whose core variant, called RIF Core , is essentially Datalog, i.e., function-free Horn logic.

title: Reasoning for Description Logics aroundSHIQ in a Resolution Framework
abstract: We present several algorithms for reasoning with description logics closely related to SHIQ. Firstly, we present an algorithm for deciding satisfiability of SHIQ knowledge bases. Then, to enable representing concrete data such as strings or integers, we devise a general approach for reasoning with concrete domains in the framework of resolution, and apply it to obtain a procedure for deciding SHIQ(D). For unary coding of numbers, this procedure is worst-case optimal, i.e. it runs in exponential time. Motivated by the prospects of reusing optimization techniques from deductive databases, such as magic sets, we devise an algorithm for reducing SHIQ(D) knowledge bases to disjunctive datalog programs. Furthermore, we show that so-called DL-safe rules can be combined with disjunctive programs obtained by our transformation to increase the expressivity of the logic, without affecting decidability. We show that our algorithms can easily be extended to handle answering conjunctive queries over SHIQ(D) knowledge bases. Finally, we extend our algorithms to support metamodeling. Since SHIQ(D) is closely related to OWL-DL, our algorithms provide alternative mechanisms for reasoning in the Semantic Web.

title: Reasoning in description logics using resolution and deductive databases
abstract: Description logics (DLs) are knowledge representation formalisms with well-understood model-theoretic semantics and computational properties. The DL SHIQ(D) provides the logical underpinning for the family of Semantic Web ontology languages. Metadata management applications, such as the Semantic Web, often require reasoning with large quantities of assertional information; however, existing algorithms for DL reasoning have been optimized mainly for efficient terminological reasoning. Although techniques for terminological reasoning can be used for assertional reasoning as well, they often do not exhibit good performance in practice. Deductive databases are knowledge representation systems specifically designed to efficiently reason with large data sets. To see if deductive database techniques can be used to optimize assertional reasoning in DLs, we studied the relationship between the two formalisms. Our main result is a novel algorithm that reduces a SHIQ(D) knowledge base KB to a disjunctive datalog program DD(KB) such that KB and DD(KB) entail the same set of ground facts. In this way, we allow DL reasoning to be performed in DD(KB) using known, optimized algorithms. The reduction algorithm is based on several novel results. In particular, we developed a resolution-based algorithm for deciding satisfiability of SHIQ knowledge bases. Furthermore, to enable representation of concrete data, such as strings or integers, we developed a general approach for reasoning with concrete domains in the framework of resolution, and we use it to extend our algorithms to SHIQ(D). For unary coding of numbers, these algorithms run in exponential time, and are thus worst-case optimal. These results allowed us to derive tighter data complexity bounds. Namely, assuming that the size of the assertional knowledge dominates the size of the terminological knowledge, the reduction algorithm runs in nondeterministic polynomial time; furthermore, if disjunctions are not used, it runs in deterministic polynomial time. Finally, we extended these algorithms in several ways. First, we showed that socalled DL-safe rules can be combined with disjunctive programs obtained by the reduction to increase the expressivity of the logic, without affecting decidability. Second, we derived an algorithm for answering conjunctive queries. Third, we extended the algorithms to support metamodeling. To estimate the practicability of our algorithms, we implemented KAON2—a new DL reasoning system. Our experiments show a performance increase in query answering over existing DL systems of one or more orders of magnitude.

title: A Resolution-Based Decision Procedure for SHOIQ
abstract: We present a resolution-based decision procedure for the description logic SHOIQ-the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for deriving saturation-based decision procedures to SHOIQ, is not straightforward due to nominals, number restrictions, and inverse roles-a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus, extended with custom simplification rules.

title: Efficient Inferencing for OWL EL
abstract: We develop inferencing methods for SROEL(∩, ×) - a DL that subsumes the main features of the W3C recommendation OWL EL -, and present a framework for studying materialisation calculi based on datalog. The latter is used to investigate the resource requirements for inferencing, and we can show that certain SROEL(∩, ×) feature combinations must lead to increased space upper bounds in any materialisation calculus, suggesting that efficient implementations are easier to obtain for suitably chosen fragments of SROEL(∩, ×).

title: Practical Reasoning with Nominals in the EL Family of Description Logics
abstract: The EL family of description logics (DLs) has been designed to provide a restricted syntax for commonly used DL constructors with the goal to guarantee polynomial complexity of reasoning. Yet, polynomial complexity does not always mean that the underlying reasoning procedure is efficient in practice. In this paper we consider a simple DL ELO from the EL family that admits nominals, and argue that existing polynomial reasoning procedures for ELO can be impractical for many realistic ontologies. To solve the problem, we describe an optimization strategy in which the inference rules required for reasoning with nominals are avoided as much as possible. The optimized procedure is evaluated within the reasoner ELK and demonstrated to perform well in practice.

title: Concurrent Classification of EL Ontologies
abstract: We describe an optimised consequence-based procedure for classification of ontologies expressed in a polynomial fragment \({\mathcal{ELH_{R^+}}}\) of the OWL 2 EL profile. A distinguishing property of our procedure is that it can take advantage of multiple processors/cores, which increasingly prevail in computer systems. Our solution is based on a variant of the ‘given clause’ saturation algorithm for first-order theorem proving, where we assign derived axioms to ‘contexts’ within which they can be used and which can be processed independently. We describe an implementation of our procedure within the Java-based reasoner ELK. Our implementation is light-weight in the sense that an overhead of managing concurrent computations is minimal. This is achieved by employing lock-free data structures and operations such as ‘compare-and-swap’. We report on preliminary experimental results demonstrating a substantial speedup of ontology classification on multi-core systems. In particular, one of the largest and widely-used medical ontologies SNOMED CT can be classified in as little as 5 seconds.

title: Local closed world reasoning with description logics under the well-founded semantics
abstract: An important question for the upcoming Semantic Web is how to best combine open world ontology languages, such as the OWL-based ones, with closed world rule-based languages. One of the most mature proposals for this combination is known as hybrid MKNF knowledge bases (Motik and Rosati, 2010 ), and it is based on an adaptation of the Stable Model Semantics to knowledge bases consisting of ontology axioms and rules. In this paper we propose a well-founded semantics for nondisjunctive hybrid MKNF knowledge bases that promises to provide better efficiency of reasoning, and that is compatible with both the OWL-based semantics and the traditional Well-Founded Semantics for logic programs. Moreover, our proposal allows for the detection of inconsistencies, possibly occurring in tightly integrated ontology axioms and rules, with only little additional effort. We also identify tractable fragments of the resulting language.

title: Consequence-Based Reasoning beyond Horn Ontologies
abstract: Consequence-based ontology reasoning procedures have so far been known only for Horn ontology languages. A difficulty in extending such procedures is that non-Horn axioms seem to require reasoning by case, which causes non-determinism in tableau-based procedures. In this paper we present a consequence-based procedure for ALCH that overcomes this difficulty by using rules similar to ordered resolution to deal with disjunctive axioms in a deterministic way; it retains all the favourable attributes of existing consequence-based procedures, such as goal-directed "one pass" classification, optimal worst-case complexity, and "pay-as-you-go" behaviour. Our preliminary empirical evaluation suggests that the procedure scales well to non-Horn ontologies.

title: Hypertableau Reasoning for Description Logics
abstract: We present a novel reasoning calculus for the description logic SHOIQ+--a knowledge representation formalism with applications in areas such as the SemanticWeb. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions--a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.