In this paper we present three results concerning the unification problem in the descriptionℱloℒgi⊥c. The logic ℱ ℒ⊥ is a sub-Boolean logic that supports only conjunction, value restrictions, and the top and bottom constructors, without any form of negation. Subsumptioℱn ℒin⊥ can be decided in polynomial time. Although we do not solve the unification problem itself, we establish three related findings. First, we show that unification in ℱ ℒ⊥ is of type nullary, a result inspired by a similar theorem for the modal logic K. Second, we reduce the unification problem in ℱ ℒ⊥ to the unification problem inℱ ℒ0, equipped with a forward TBox. Third, we revisit the known result that the matching probleℱmℒin⊥ can be solved in polynomial time and provide a new to-implement algorithm which solves the matching probleℱm ℒin⊥ in polynomial time. In this paper, we focus on a small description logℱic,ℒ⊥, which extends the constructors of its sister logic ℱ ℒ0 by adding the bottom concept. We present three results: the unification tyℱpeℒo⊥f is nullary, inspired by a similar result for the modal log ic(see [1]); the unification problem inℱ ℒ⊥ can be reduced to the one iℱn ℒ0 with a special TBox, corresponding t2o][; and we present a simple2. The description logics ℱ ℒ0 and ℱ ℒ⊥ (∀ .) = (∀ 1∀ 2 … ∀ .) where = 1 … ∈ +. refered to as concept names and role names, by the following grammar: All notions in this chapter are introducedℱfoℒr⊥. To obtain their equivalents ℱinℒ0, simply omit ⊥. In the description logiℱc ℒ⊥, (complex) concepts are generated from two disjoint s e tsand , An interpretation of conceptsℱinℒ⊥ is a pair = (Δ , ⋅ ), where Δ is a non-empty domain of elements and⋅ is an interpreting function defined on concept names and role names as foll⊤ow=: Δ ; Proceedings ceur-ws.org
algorithm for it. description logic, unification type
= ∩ ; (∀ .) = { ∈ Δ ∣ ∀ ∈ Δ [(, ) ∈ → ∈ ]}; ; ⊆ Δ
× Δ , for any ∈ , and extended to all complex concepts
A concept may be reduced with the following reductions to an equivalent concept (interpreted by the same set in any interpretation⊓)⊤:, ⊤ ⊓ ⇝ ; ⊓ ⊥, ⊥ ⊓ ⇝ ⊥; ∀ .⊤ ⇝ ⊤; ∀ .( ⊓ ) ⇝ ∀ . ⊓ ∀ ..
We call a concep t reduced if none of the reduction rules applies.
For convenience, we will use the notatio∀n.
for the concept of the form∀: 1(∀ 2(… (∀ . ))) , where = 1 … and is either⊤ or ⊥ or a concept name . A concept of this form is calledpaarticle. This research is part of the project No 2022/47/P/ST6/03196 within the POLONEZ BIS programme cofunded by the National Science Centre and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 945339. For the purpose of Open Access, the author has applied a CC-BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission.
CEUR Workshop
ISSN1613-0073
The word over is called the role word of the particle∀ . . For role words , ′, by ≤ ′ we denote tha t is a prefix of ′.
It is easy to see that any concept is equivalent to a conjunction of pa r=ti∀cles1,. 1 ⊓ ⋯ ⊓ ∀ . , where 1, … , are possibly empty words over . In fact because of properties of conjunction, we identify a reduced concept with a set of particles in such a conjunction.
Let be an ℱ ℒ⊥-reduced concept. We define () (role depth) and() (size) recursively: if = or = ⊤ or = ⊥ , then () = () = 0; if = ⊓ , then () = ({ (), ()}) and () = () + (); if = ∀ . ′, () = ( ′) + 1 and () = ( ′) + 1.
Subsumption between concepts ⊑ obtains if for all interpretation s, ⊆ . Equivalence: ≡ if ⊑ and ⊑ . For any concept, we have ⊥ ⊑ and ⊑ ⊤. In ℱ ℒ⊥, let and = { 1, … , } be reduced concepts. The n⊑ iif for every ∈ , one of the following holds: (1) ∈ , (2) = ∀ . , where is a concept name o⊥r, and there exist∀s ′.⊥ ∈ such that′ ≤ .
In order to define a unification problem, we partition the set of concept na m es into two disjoint sets: variables ( ) and constant s ( ). A variable is thus a concept name that may be substituted by any concept while a constant cannot be substituted.
A substitution is a mapping from to the set of aℱll ℒ⊥-concepts. It is extended to all concepts in the usual way. Theunification problem (unification problem ) is defined by its input Γ = { 1 ⊑? 1, … , ⊑? }; and the output is “yes” if there is a substitution that makes these subsumptions true, or “no” otherwise. Without loss of generality, we can assume t1h, a…t, are particles. A substitutio nis a unifier for the unification problemΓ = { 1 ⊑? 1, … , ⊑? } if ( 1) ⊑ ( 1), … , ( ) ⊑ ( ). In this case, we say that the problemu nisifiable .
LetΓ be an unification problem with the set of variabl esand unifiers , . We say tha t is more general than (or is less general than ), if there is a substituti onsuch that( ) ≡ ( ( )), for all ∈ . If a unifier is more general than any other unifier, we call it maost general unifier (an mgu) ofΓ.
A setΠ of unifiers of a given unification problem Γ is called acomplete set of unifiers if every unifier of Γ is less general than some element oΠf. For a given unification problemΓ we define four unification types (from ”best” to ”worst”) based on the existence and cardinality of its complete set. The problem has unification type:unitary if there exists complete set of unifiers consisting of one unifie ;r ifnitary if it has finite compete set of unifiers, but has no most general unifieri;nfinitary if it has an infinite minimal complete set of unifiers;nullary (or zero) if it has no minimal complete set of unifiers. The unification type of a logic ℱ( ℒ⊥ in our case) is the worst unification type of its unifiable problems.
In this section, we sketch a prove thℱaℒt⊥ has nullary unification type by showing that the unification problem Γ = { ⊑ ? ∀ . } has no minimal complete set of unifiers. To this end, we introduce the set of substitutions consisting of: 0( ) = ⊥; ( ) = ⊓ ∀ . ⊓ … ⊓ ∀ −1 . ⊓ ∀ .⊥, for ≥ 1; ⊤( ) = ⊤.
One can easily check th at( ) ⊑ (∀ . ), for each ∈ ℕ ∪ {⊤}.
It can also be shown that the seits complete forΓ. Let be a unifier for Γ not equal t o ⊤ and let ∈ where = ( ( )). Then ( ) ≡ ( ( )).
At this point we know th atis a complete set of unifiers ofΓ. To complete the argument, we observe that there is no minimal complete set of unifiers fΓo.rIt can be easily shown tha t+:1 is more general tha t , but is not more general tha n+1 , for each ≥ 0. Using a proof by contradiction we obtain the result: Theorem 1. The type of the unification problem Γ is nullary. 5. Reduction from ℱ ℒ⊥ to ℱ ℒ0 with a TBox A ℱ ℒ0 TBox (TBox for short) is a finite set ofℱ ℒ0-subsumptions. A model of a TBox is an interpretation such tha t ⊆
for all ⊑ ∈ . subsumed by
w.r.t. a TBox unifier of a unification problem Γ w.r.t. a TBox if () ⊑
Let and
be concepts. We say tha t is (written ⊑ ) if ⊆ for each model of .
We say that is a () for each ⊑ ∈ Γ.
TBox:
Σ = { ⊑ ∣ henceforth denote cept names:
Let be an ℱ ℒ⊥ concept, and be a constant, that does not appear. inBy we denote the ℱ ℒ0-concept obtained fro m by replacing all occurrences o⊥f with the constan.tFor = ⊑ , =
⊑ . Given a finite set Γ of ℱ ℒ⊥-subsumptions, we define the corresponding setΓ of ℱ ℒ0-subsumptions byΓ
= { ∣ ∈ Γ}. For a given finite set of subsumptionsΓ, (Γ) is the set of all concept names occuring iΓn, (Γ) is the set of all role names occuring iΓn.For a given signature Σ =< , >, where is a finite subset of and is a finite subset of , we define the following for every ∈ } ∪ { ⊑ ∀. ∣
for every ∈ }. To simplify notation, we < ({}), ({})> as , and express< (Γ), (Γ) > as Σ(Γ).
The following theorem is similar to Lemm2a.2 in [2], which considers subsumptions between conTheorem 2. An ℱ ℒ⊥-subsumption of the form ⊑ obtains if ⊑ . {( ( ))
where is in domain of } , then the signature ofis contained inΣ(Γ). Therefore:
If is a unifier of an ℱ ℒ⊥ unification problem Γ of the minimal size where size of is sum of ℱ ℒ0-unifier w.r.t. the TBox Σ(Γ).
Theorem 3. Let Γ be a unification problem in ℱ ℒ⊥. Then Γ has an ℱ ℒ⊥-unifier if Γ has an dificult than unification in ℱ ℒ⊥.
We showed that the unification problem iℱn ℒ⊥ can be reduced to a unification problem inℱ ℒ0 with a TBox. This does not give us a solution for the unificationℱinℒ⊥, since unification inℱ ℒ0 with a TBox is not solved. However, it show that the unification problemℱ iℒn0 with a TBox is more
The matching problem is a special kind of a unification probl em≡ ? , where contains no variables. In [3], it was shown that, with respect to general TBoxes, matching is ExpTime-complℱetℒe0in, whereas for a restricted form of TBoxes, namelfyorward TBoxes, the complexity drops to PSpace. We can transfer this result tℱoℒ⊥ via Theorem 3, obtaining that matchingℱinℒ⊥ is in PSpace. In [4] (see Theorem 3.8) it was shown that matchingℱinℒ⊥ is polynomial. Here, we present another simple-to-implement algorithm which solves the matching probleℱm ℒin⊥ in polynomial time. Algorithm 1 Matching Input: ≡ ? ,
where does not contain variabl es=, ⊓∀ Output: True if there is a matcher, False otherwise. are (not necessarily diferent) variables, and1, … , are words over . 1: procedure Matching( ≡ ? ) 1 . 1 ⊓⋯⊓∀ . , where does not contain variabl es,1, … , 2: 3: 4: 5: 6: 7: 8: 9: if ⋢ else
then return False return True for all ∀. ∈ such that∀. ∉
and there is no∀ ′.⊥ ∈ where ′ ≤ do return False if no ∀ . is found then
Find ∀ . such that ≤ ( is a prefix of )
One can see that the algorithm must terminate in time polynomial in the size of the problem. In order to justify the correctness of Algorith1mwe define a special substitutio n̂ . For every occurring in , (̂ ) ∶=
⨅{∀. ∣ ∀ . ∈ matching problem ≡ ? and∀. ∈
where is a constant o⊥r}. Next we prove that a has a unifier if the substitution ̂ is a unifier. The correctness follows from the fact that the algorithm computes the substi t̂ .ution
presented a simple algorithm that solves matching in polynomial time.
We have presented three results related to the unification problemℱiℒn⊥. The unification type of ℱ ℒ⊥ turns out to be nullary. Hencℱe, ℒ⊥ has the same type as the description logℰicℒs , ℱ ℒ0, and ℒ
. The second result, reduction of the unification problem iℱnℒ⊥ to unification inℱ ℒ0 modulo a TBox Σ implies that the unification problem iℱn ℒ⊥ is easier than the one iℱn ℒ0 with a TBox. It is even easier than the unification ℱinℒ0 with a forward TBox. As the third result, we have
During the preparation of this work, the authors used ChatGPT based on GPT-4o in order to: Grammar and spelling check. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.