scholarly journals Towards a Practical Decision Procedure for Uniform Interpolants of EL-TBoxes - a Proof-Theoretic Approach

10.29007/bsqm ◽  
2018 ◽  
Author(s):  
Michel Ludwig ◽  
Dirk Walther
Keyword(s):  
Decision Procedure ◽  
Description Logic ◽  
Graph Representation ◽  
Theoretic Approach ◽  
Biomedical Ontologies ◽  
Prototype Implementation

We show how the problem of deciding the existence of uniform interpolants of TBoxes formulated in the Description Logic \EL can be divided into three subproblems based on a characterisation of the logical difference between \EL-TBoxes. We propose a proof-theoretic decision procedure for subsumer interpolants of general TBoxes formulated in the Description Logic \EL, solving one of these subproblems. A subsumer interpolant of a TBox depends on a signature and on a concept name. It is a TBox formulated using symbols from the signature only such that, both, it follows from the original TBox and it exactly entails the subsumers formulated in the signature that follow from the concept name \wrt~the original TBox. Our decision procedure first constructs a graph that exactly represents the part of original TBox that is describable using signature symbols only. Subsequently, it is checked whether a graph-representation of the original TBox can be simulated by the constructed graph, in which case a subsumer interpolant exists. We also evaluate our procedure by applying a prototype implementation on several biomedical ontologies.

A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,×

2020 ◽  
Vol 176 (3-4) ◽  
pp. 349-384
Author(s):  
Domenico Cantone ◽  
Marianna Nicolosi-Asmundo ◽  
Daniele Francesco Santamaria
Keyword(s):  
Description Logic ◽  
Description Logics ◽  
Theoretic Approach ◽  
The Novel ◽  
Data Types ◽  
Left Hand ◽  
Rule Languages ◽  
Tableau System ◽  
High Scalability ◽  
Better Than

In this paper we consider the most common TBox and ABox reasoning services for the description logic 𝒟ℒ〈4LQSR,x〉(D) ( 𝒟 ℒ D 4,× , for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR. 𝒟 ℒ D 4,× is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the SemanticWeb Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left-hand side of inclusion axioms, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic 𝒟 ℒ D 4,× . Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the γ-rule. The novel system, called KEγ-tableau, turns out to be an improvement of the system introduced in [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KEγ-tableau-based reasoner are up to about 400% better than the ones of the other two systems.

The Fuzzy Description Logic ALCFH with Hedge Algebras as Concept Modifiers

2003 ◽  
Vol 7 (3) ◽  
pp. 294-305 ◽  
Author(s):  
Steffen Hölldobler ◽  
◽  
Hans-Peter Störr ◽  
Tran Dinh Khang ◽  
Keyword(s):  
Knowledge Base ◽  
Decision Procedure ◽  
Description Logic ◽  
Ordered Set ◽  
Fuzzy Description ◽  
Linearly Ordered Set

In this paper we present the fuzzy description logic ALCFH introduced, where primitive concepts are modified by means of hedges taken from hedge algebras. ALCFH is strictly more expressive than Fuzzy-ALC defined in [11]. We show that given a linearly ordered set of hedges primitive concepts can be modified to any desired degree by prefixing them with appropriate chains of hedges. Furthermore, we define a decision procedure for the unsatisfiability problem in ALCFH, and discuss knowledge base expansion when using terminologies, truth bounds, expressivity as well as complexity issues. We extend [8] by allowing modifiers on non-primitive concepts and extending the satisfiability procedure to handle concept definitions.

scholarly journals Optimised ExpTime Tableaux for𝒮ℋℐ𝒩over Finite Residuated Lattices

2014 ◽  
Vol 2014 ◽  
pp. 1-15
Author(s):  
Jian Huang ◽  
Xinye Zhao ◽  
Jianxing Gong
Keyword(s):  
Experimental Evaluation ◽  
Decision Procedure ◽  
Description Logic ◽  
Optimization Technique ◽  
Residuated Lattices ◽  
Optimization Techniques ◽  
Satisfiability Problem ◽  
Reasoning Algorithm ◽  
De Morgan Lattice

This study proposes to adopt a novel tableau reasoning algorithm for the description logic𝒮ℋℐ𝒩with semantics based on a finite residuated De Morgan lattice. The syntax, semantics, and logical properties of this logic are given, and a sound, complete, and terminating tableaux algorithm for deciding fuzzy ABox consistency and concept satisfiability problem with respect to TBox is presented. Moreover, based on extended and/or completion-forest with a series of sound optimization technique for checking satisfiability with respect to a TBox in the logic, a new optimized ExpTime (complexity-optimal) tableau decision procedure is presented here. The experimental evaluation indicates that the optimization techniques we considered result in improved efficiency significantly.

An Efficient Approach for Ranking of Semantic Web Documents by Computing Semantic Similarity and Using HCS Clustering

2021 ◽  
Vol 5 (1) ◽  
pp. 45-56
Author(s):  
Poonam Chahal ◽  
Manjeet Singh
Keyword(s):  
Semantic Web ◽  
Semantic Similarity ◽  
Semantic Analysis ◽  
Semantic Content ◽  
Graph Representation ◽  
Graphical Form ◽  
Theoretic Approach ◽  
Connected Subgraph ◽  
Web Documents ◽  
The Web

In today's era, with the availability of a huge amount of dynamic information available in world wide web (WWW), it is complex for the user to retrieve or search the relevant information. One of the techniques used in information retrieval is clustering, and then the ranking of the web documents is done to provide user the information as per their query. In this paper, semantic similarity score of Semantic Web documents is computed by using the semantic-based similarity feature combining the latent semantic analysis (LSA) and latent relational analysis (LRA). The LSA and LRA help to determine the relevant concepts and relationships between the concepts which further correspond to the words and relationships between these words. The extracted interrelated concepts are represented by the graph further representing the semantic content of the web document. From this graph representation for each document, the HCS algorithm of clustering is used to extract the most connected subgraph for constructing the different number of clusters which is according to the information-theoretic approach. The web documents present in clusters in graphical form are ranked by using the text-rank method in combination with the proposed method. The experimental analysis is done by using the benchmark datasets OpinRank. The performance of the approach on ranking of web documents using semantic-based clustering has shown promising results.

THE NEXT GENERATION OF SIMILARITY MEASURES THAT FULLY EXPLORE THE SEMANTICS IN BIOMEDICAL ONTOLOGIES

2013 ◽  
Vol 11 (05) ◽  
pp. 1371001 ◽  
Author(s):  
FRANCISCO M. COUTO ◽  
H. SOFIA PINTO
Keyword(s):  
Description Logic ◽  
Similarity Measures ◽  
Functional Similarity ◽  
Similarity Measurement ◽  
Biomedical Ontologies ◽  
Next Generation ◽  
Current Effort ◽  
Computational Costs ◽  
Powerful Knowledge ◽  
Near Future

There is a prominent trend to augment and improve the formality of biomedical ontologies. For example, this is shown by the current effort on adding description logic axioms, such as disjointness. One of the key ontology applications that can take advantage of this effort is the conceptual (functional) similarity measurement. The presence of description logic axioms in biomedical ontologies make the current structural or extensional approaches weaker and further away from providing sound semantics-based similarity measures. Although beneficial in small ontologies, the exploration of description logic axioms by semantics-based similarity measures is computational expensive. This limitation is critical for biomedical ontologies that normally contain thousands of concepts. Thus in the process of gaining their rightful place, biomedical functional similarity measures have to take the journey of finding how this rich and powerful knowledge can be fully explored while keeping feasible computational costs. This manuscript aims at promoting and guiding the development of compelling tools that deliver what the biomedical community will require in a near future: a next-generation of biomedical similarity measures that efficiently and fully explore the semantics present in biomedical ontologies.

scholarly journals A Practical Approach to Forgetting in Description Logics with Nominals

2020 ◽  
Vol 34 (03) ◽  
pp. 3073-3079
Author(s):  
Yizheng Zhao ◽  
Renate Schmidt ◽  
Yuejie Wang ◽  
Xuanming Zhang ◽  
Hao Feng
Keyword(s):  
Description Logic ◽  
Description Logics ◽  
Practical Method ◽  
Practical Approach ◽  
Ontology Engineering ◽  
Success Rates ◽  
Prototype Implementation ◽  
Speed Up

This paper investigates the problem of forgetting in description logics with nominals. In particular, we develop a practical method for forgetting concept and role names from ontologies specified in the description logic ALCO, extending the basic ALC with nominals. The method always terminates, and is sound in the sense that the forgetting solution computed by the method has the same logical consequences with the original ontology. The method is so far the only approach to deductive forgetting in description logics with nominals. An evaluation of a prototype implementation shows that the method achieves a significant speed-up and notably better success rates than the Lethe tool which performs deductive forgetting for ALC-ontologies. Compared to Fame, a semantic forgetting tool for ALCOIH-ontologies, better success rates are attained. From the perspective of ontology engineering this is very useful, as it provides ontology curators with a powerful tool to produce views of ontologies.

scholarly journals On Concept Forgetting in Description Logics with Qualified Number Restrictions

2018 ◽  
Author(s):  
Yizheng Zhao ◽  
Renate Schmidt
Keyword(s):  
Description Logic ◽  
Description Logics ◽  
Practical Method ◽  
Test Cases ◽  
Biomedical Ontologies ◽  
Large Corpus

This paper presents a practical method for computing solutions of concept forgetting in the description logic ALCOQ(neg,and,or), basic ALC extended with nominals, qualified number restrictions, role negation, role conjunction and role disjunction. The method is based on a non-trivial generalisation of Ackermann's Lemma, and attempts to compute either semantic solutions of concept forgetting or uniform interpolants in ALCOQ(neg,and,or). It is so far the only approach to concept forgetting in description logics with number restrictions plus nominals, as well as in description logics with ABoxes. Results of an evaluation with a prototypical implementation have shown that the method was successful in more than 90% of the test cases from a large corpus of biomedical ontologies. In only 13.2% of these cases the solutions were semantic solutions.

Sign in / Sign up

Export Citation Format

Share Document