Reasoning on vague ontologies using rough set theory

Web ontologies can contain vague concepts, which means the knowledge about them is imprecise and then query answering will not possible due to the open world assumption. A concept description can be very exact (crisp concept) or exact (fuzzy concept) if its knowledge is complete, otherwise it is inexact (vague concept) if its knowledge is incomplete. In this paper, we propose a method based on the rough set theory for reasoning on vague ontologies. With this method, the detection of vague concepts will insert into the original ontology new rough vague concepts where their description is defined on approximation spaces to be used by extended Tableau algorithm for automatic reasoning. The extended Tableau algorithm by this rough set-based vagueness is intended to answer queries even with the presence of incomplete information.

Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach

When modeling real-world domains, we have to deal with information that is incomplete or that comes from sources with different trust levels. This motivates the need for managing uncertainty in the Semantic Web. To this purpose, we introduced a probabilistic semantics, named DISPONTE, in order to combine description logics (DLs) with probability theory. The probability of a query can be then computed from the set of its explanations by building a Binary Decision Diagram (BDD). The set of explanations can be found using thetableau algorithm, which has to handle non-determinism. Prolog, with its efficient handling of non-determinism, is suitable for implementing the tableau algorithm. TRILL and TRILLPare systems offering a Prolog implementation of the tableau algorithm. TRILLPbuilds apinpointing formulathat compactly represents the set of explanations and can be directly translated into a BDD. Both reasoners were shown to outperform state-of-the-art DL reasoners. In this paper, we present an improvement of TRILLP, named TORNADO, in which the BDD is directly built during the construction of the tableau, further speeding up the overall inference process. An experimental comparison shows the effectiveness of TORNADO. All systems can be tried online in the TRILL on SWISH web application athttp://trill.ml.unife.it/.

Reasoning in the presence of inconsistency through Preferential ALC

This paper presents an inconsistency tolerant semantics for the Description Logic ALC called Preferential ALC (p-ALC). A p-ALC knowledge base is comprised of defeasible and non-defeasible axioms. The defeasible ABox and TBox are labelled with confidence weights that could reflect an axiom's provenance. Entailment is defined through the notion of preferred interpretations which minimise the total weight of the inconsistent axioms. We introduce a modified ALC tableau algorithm in which the open branches give rise to the preferred interpretations, and show that it can compute p-ALC entailment by refutation. The modified algorithm is implemented as an incremental answer set program (ASP) that exploits optimisation to capture preferred interpretations of p-ALC.

Reasoning with Vague Concepts in Description Logics

The open world assumption in ontologies representing knowledge may assign deficient (imprecise) meaning for ontology concepts which are language adjectives referring the meaning of classes of objects (individuals). The interpretation of an imprecise (vague) concept is by three subsets of individuals. The first subset of individuals surely belongs to the vague concept, the second subset of individuals surely doesn't belong the vague concept and the third subset is in the borderline. In this paper, the authors will show that is possible to describe ontology vague concepts using well-defined formal languages. The authors will propose also an extension of the Tableau algorithm for reasoning over vague ontologies.

A Decidable Extension of SROIQ with Complex Role Chains and Unions

We design a decidable extension of the description logic SROIQ underlying the Web Ontology Language OWL 2. The new logic, called SR+OIQ, supports a controlled use of role axioms whose right-hand side may contain role chains or role unions. We give a tableau algorithm for checking concept satisfiability with respect to SR+OIQ ontologies and prove its soundness, completeness and termination.