Unification in ℰ ℒℋℛ+ without the Top Concept modulo Cycle-Restricted Ontologies (Extended Abstract)

Abstract

Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL ℰℒ is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

Keywords

• eol>Unification
• Description Logics
• Complexity

-

and the second one by

Unification in the DLs ℰ ℒ and ℰ ℒ⊤−

Unification in the DL ℰ ℒ (which provides the concept constructors conjunction ⊓, existential restriction ∃., and top concept ⊤) was first investigated in [ 3 ], where it was proved that deciding unifiability is an NP-complete problem. The NP upper bound was shown in that paper using a brute-force “guess and then test” NP algorithm. More practical algorithms for solving this problem and for computing unifiers were presented in [ 4 ] and [ 5 ], where the former describes a goal-oriented transformation-based algorithm and the latter is based on a translation to SAT. Implementations of these two algorithms are provided by the system UEL2 [ 6 ], which is also available as a plug-in for the ontology editor Protégé. At the time these algorithms were developed, SNOMED CT was an ℰ ℒ ontology consisting of acyclic concept definitions. Since such definitions can be encoded into the unification problem (see Section 2.3 in [ 4 ]), algorithms for unification of ℰ ℒ concept descriptions (without background ontology) could be applied to SNOMED CT.

There was, however, one problem with employing these algorithms in the context of SNOMED CT: the top concept is not used in SNOMED CT, but the concepts generated by ℰ ℒ unification might contain ⊤, even if applied to concept descriptions not containing ⊤. Thus, the concept descriptions produced by the unifier are not necessarily in the style of SNOMED CT. For example, assume that we are looking for a unifier satisfying the two subsumption constraints 3 ∃findingSite.LungStructure ⊑? ∃findingSite., ∃findingSite.HeartStructure ⊑? ∃findingSite..

It is easy to see that there is only one unifier of these two constraints, which replaces with ⊤. Unification in ℰ ℒ⊤− , i.e., the fragment of ℰ ℒ in which the top constructor is disallowed, was investigated in [ 8, 9 ]. Surprisingly, it turned out that the absence of ⊤ makes unification considerably harder, both from a conceptual and a computational complexity point of view. In fact, the complexity of deciding unifiability increases from NP-complete for ℰ ℒ to PSpace-complete for ℰ ℒ⊤− . The unification algorithm for ℰ ℒ⊤− introduced in [ 8, 9 ] basically proceeds as follows. It first applies the unification algorithm for ℰ ℒ to compute so-called local unifiers. If none of them is an ℰ ℒ⊤− -unifier, then it tries to augment the images of the variables by conjoining a special kind of concept descriptions called particles. The task of ifnding appropriate particles is reduced to solving certain systems of linear language inclusions, which can be realized in PSpace using an automata-based approach.

Extending unification in ℰ ℒ towards background ontologies

The current version of SNOMED CT consists not only of acyclic concept definitions, but also contains more general concept inclusions (GCIs). In addition, properties of the part-of relation are no longer encoded using the so-called SEP-triplet encoding [ 10 ], but are directly expressed via role axioms [ 11 ], which can, for instance, be used to state that the part-of relation is transitive and that proper-part-of is a subrole of part-of.

Decidability of unification in ℰ ℒ w.r.t. a background ontology consisting of GCIs is still an open problem. In [ 7 ], it is shown that the problem remains in NP if the ontology is cycle-restricted, which is a condition that the current version of SNOMED CT satisfies. An ontology is called cycle-restricted if it does not entail cyclic subsumptions of the form ⊑ ∃1.∃2. · · · ∃ ., where ≥ 1 and is an ℰ ℒ concept description. Extensions of the result shown in [ 7 ] to the DL ℰ ℒℋℛ+ , which additionally allows for transitive roles and role inclusion axioms, were presented in [ 12 ] and [ 13 ], where the former introduces a SAT-based algorithm and the latter a transformation-based one. However, in all these algorithms, unifiers may introduce concept descriptions containing ⊤. In our example with the diferent 2https://sourceforge.net/projects/uel/ 3Instead of equivalence constraints, as in our above example and in early work on unification in DLs, we consider here a set of subsumption constraints as unification problem. It is easy to see that these two kinds of unification problems can be reduced to each other [ 7 ]. ifnding site, however, the presence of the GCIs

LungStructure ⊑ UpperBodyStructure and HeartStructure ⊑ UpperBodyStructure would yield a unifier not using

⊤, namely the one that replaces with UpperBodyStructure.

Our new contribution

The purpose of the work we report on here is to investigate the unification problem in the DL ℰ ℒℋ⊤−ℛ+ w.r.t. cycle-restricted ontologies. Our main result is that the presence of a cycle-restricted ontology does not increase the complexity of unification in ℰ ℒ without top, i.e., the unification decision problem remains in PSpace.

Theorem 1. Deciding unifiability of ontologies is PSpace-complete.

ℰ ℒℋ⊤−ℛ+ -unification problems w.r.t. cycle-restricted ℰ ℒℋ⊤−ℛ+

To obtain this result, we combine the approach for unification in ℰ ℒ⊤− [ 8, 9 ] with the one for unification in ℰ ℒℋℛ+ w.r.t. cycle-restricted ontologies [ 7, 12, 13 ], to devise a non-deterministic polynomial space unification algorithm for ℰ ℒℋℛ

⊤− + w.r.t. cycle-restricted ontologies. This algorithm follows the line of the one for ℰ ℒ⊤− in that it basically first generates ℰ ℒℋℛ+ -unifiers, which it then tries to pad with particles. Appropriate particles are found as solutions of certain linear language inclusions. However, due to the presence of GCIs and role axioms, quite a number of non-trivial changes and additions are required. In particular, the solutions of the systems of linear language inclusions as constructed in [ 8, 9 ] cannot capture particles that are appropriate due to the presence of an ontology. For instance, in our example, UpperBodyStructure would be such a particle. To repair this problem, we first need to show that, in ℰ ℒℋℛ

⊤− + , unifiability w.r.t. a cycle-restricted ontology can be characterized by the existence of a special type of unifiers. Afterwards, we exploit the properties of this kind of unifiers to define more sophisticated systems of language inclusions, which encode the semantics of GCIs and role axioms occurring in a background ontology. The solutions of such systems then yield also particles that are appropriate only due to the presence of this ontology.

Future Work

With SNOMED CT in mind, it would be interesting to see whether results on unification (with or without top) can be further extended to ontologies additionally containing so-called right-identity rules, i.e., role axioms of the form ∘ ⊑ , since they are also needed to get rid of the SEP-triplet encoding mentioned above. However, this would require to extend the characterization of subsumption (between ℰ ℒ concepts w.r.t. a background ontology) to this setting, which is probably a non-trivial problem. From a theoretical point of view, the big open problem is whether one can dispense with the requirement that the ontology must be cycle-restricted. Even for pure ℰ ℒ, decidability of unification w.r.t. unrestricted ontologies is an open problem.

From a practical point of view, the next step is to develop an algorithm that replaces non-deterministic guessing by a more intelligent search procedure. Since the unification problem is PSpace-complete, a polynomial-time translation of the whole problem into SAT is not possible (unless NP = PSpace). However, one could try to delegate the search for an ℰ ℒℋℛ+ -unifier to a SAT solver, which interacts with a solver for the additional condition on such a unifier (existence of a certain type of solution for the corresponding system of linear language inclusions) in an SMT-like fashion [ 14 ].

The paper summarized by this abstract has been accepted for publication at IJCAR 2024 [ 15 ]. The extended version [16] of [ 15 ] provides detailed proof of our results.

Acknowledgments This work was partially supported by the German Federal Ministry of Education and Research (BMBF, SCADS22B) and the Saxon State Ministry for Science, Culture and Tourism (SMWK) by funding the competence center for Big Data and AI “ScaDS.AI Dresden/Leipzig”. The authors would like to thank Stefan Borgwardt and Francesco Kriegel for helpful discussions on the form of the definitions and axioms used in the current version of SNOMED CT. Conference, IJCAR 2024, Nancy, France, July 1-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, Springer, 2024, pp. 279–297. [16] F. Baader, O. Fernández Gil, Unification in the Description Logic ℰ ℒℋℛ+ without the Top Concept modulo Cycle-Restricted Ontologies (Extended Version), LTCS-Report 24-01, Chair for Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2024. URL: https://lat.inf.tu-dresden.de/research/reports.html.

References

[1] F. Baader , P. Narendran , Unification of concept terms in description logics , J. Symb. Comput . 31 ( 2001 ) 277 - 305 .

[2] F. Baader , S. Borgwardt , B. Morawska , Constructing SNOMED CT Concepts via Disunification , LTCS-Report 17-07 , Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017 . doi: 10 .25368/ 2022 .237.

[3] F. Baader , B. Morawska , Unification in the description logic ℰ ℒ, in: Rewriting Techniques and Applications , 20th International Conference, RTA 2009, Proceedings , volume 5595 of Lecture Notes in Computer Science, Springer, 2009 , pp. 350 - 364 .

[4] F. Baader , B. Morawska , Unification in the description logic ℰ ℒ, Log . Methods Comput. Sci. 6 ( 2010 ).

[5] F. Baader , B. Morawska , SAT encoding of unification in ℰ ℒ, in: Logic for Programming , Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings , volume 6397 of Lecture Notes in Computer Science, Springer, 2010 , pp. 97 - 111 .

[6] F. Baader , J. Mendez , B. Morawska, UEL: unification solver for the description logic ℰ ℒ - system description , in: Automated Reasoning - 6th International Joint Conference, IJCAR 2012 , Proceedings , volume 7364 of Lecture Notes in Computer Science, Springer, 2012 , pp. 45 - 51 .

[7] F. Baader , S. Borgwardt , B. Morawska , Extending unification in ℰ ℒ towards general tboxes , in: Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012 , Rome, Italy, June 10-14, 2012 , AAAI Press, 2012 .

[8] F. Baader , N. T. Binh , S. Borgwardt , B. Morawska , Unification in the description logic ℰ ℒ without the top concept , in: Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011 ), volume 6803 of Lecture Notes in Computer Science, Springer-Verlag, 2011 , pp. 70 - 84 .

[9] F. Baader , T. B. Nguyen , S. Borgwardt , B. Morawska , Deciding unifiability and computing local unifiers in the description logic ℰ ℒ without top constructor , Notre Dame J. Formal Log . 57 ( 2016 ) 443 - 476 .

[10] S. Schulz , M. Romacker , U. Hahn, Part-whole reasoning in medical ontologies revisited-introducing SEP triplets into classification-based description logics , in: AMIA 1998 , American Medical Informatics Association Annual Symposium , AMIA, 1998 .

[11] B. Suntisrivaraporn , F. Baader , S. Schulz , K. A. Spackman , Replacing SEP-triplets in SNOMED CT using tractable description logic operators , in: 11th Conference on Artificial Intelligence in Medicine, AIME 2007 , Proceedings , volume 4594 of Lecture Notes in Computer Science, Springer, 2007 , pp. 287 - 291 .

[12] F. Baader , S. Borgwardt , B. Morawska , SAT encoding of unification in ℰ ℒℋℛ+ w .r.t. cyclerestricted ontologies, in: Automated Reasoning - 6th International Joint Conference, IJCAR 2012 , Proceedings , volume 7364 of Lecture Notes in Computer Science, Springer, 2012 , pp. 30 - 44 .

[13] F. Baader , S. Borgwardt , B. Morawska , A goal-oriented algorithm for unification in ℰ ℒℋℛ+ w .r.t. cycle -restricted ontologies , in: AI 2012: Advances in Artificial Intelligence - 25th Australasian Joint Conference, Proceedings , volume 7691 of Lecture Notes in Computer Science, Springer, 2012 , pp. 493 - 504 .

[14] C. W. Barrett , R. Sebastiani , S. A. Seshia , C. Tinelli , Satisfiability modulo theories , in: A. Biere , M. Heule , H. van Maaren, T. Walsh (Eds.), Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021 , pp. 1267 - 1329 . doi: 10 . 3233/FAIA201017.

[15] F. Baader , O. Fernández Gil , Unification in the Description Logic ℰ ℒℋℛ+ without the Top Concept Modulo Cycle-Restricted Ontologies , in: Automated Reasoning - 12th International Joint