Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor (Q2374390)

\(\mathcal{EL}\) is the description logic built over two disjoint sets \(N_C\) and \(N_R\) of concept and role names, respectively, whose concept terms are of the form \(\top\) (the top concept), or \(c\) for \(c\in N_C\), or \(C\sqcap D\) with \(C\) and \(D\) concept terms, or \(\exists r.C\) for \(r\in N_R\) with \(C\) a concept term. The description logic \(\mathcal{EL}^{-\top}\) is the same except that \(\top\) is not a concept term. For instance, the concept of persons having a son, a daughter and a job can be expressed in \(\mathcal{EL}\) as \[ \mathrm{Person}\sqcap\exists\mathrm{child}.\mathrm{Male}\sqcap\exists\mathrm{child}.\mathrm{Female}\sqcap\exists\mathrm{job}.\top, \] whereas the concept of female professors can be expressed in \(\mathcal{EL}^{-\top}\) as either \[ \mathrm{Person}\sqcap\mathrm{Female}\sqcap\exists\mathrm{job}.\mathrm{Professor} \] or \[ \mathrm{Woman}\sqcap\exists\mathrm{job}.\mathrm{Teacher}\sqcap\mathrm{Researcher}, \] by substituting \(\mathrm{Teacher}\sqcap\mathrm{Researcher}\) for \(\mathrm{Professor}\) and \(\mathrm{Person}\sqcap\mathrm{Female}\) for \(\mathrm{Woman}\). This is an instance of \textit{unification}, where two concept terms are made equivalent by letting some concept names, treated as variables, be replaced by concept terms. In [\textit{F. Baader} and \textit{B. Morawska}, Lect. Notes Comput. Sci. 5595, 350--364 (2009; Zbl 1242.68300)], it was shown that deciding whether two concept terms in \(\mathcal{EL}\) are unifiable is NP-complete. Motivated by the existence of SNOMED CT, a large medical ontology all of whose concepts are expressed in \(\mathcal{EL}^{-\top}\), the authors show that, surprisingly, deciding whether two concept terms in \(\mathcal{EL}^\top\) are unifiable, is harder, namely \textsc{PSpace}-complete. The proof makes use of \textit{alternating finite automata}, that can make two kinds of transitions: nondeterministic transitions that ``guess'' the next state of the automaton, and ``universal'' transitions that force the automaton to explore every possible successor state. The authors also observe that unification in \(\mathcal{EL}^{-\top}\) {\parindent=0.6cm\begin{itemize}\item[{\(\bullet\)}] is equivalent to unification modulo the equational theory \(\mathrm{SLmO}\) of \textit{semilattices with monotone operators}, defined by the identities (1) \(x\wedge(y\wedge z)=(x\wedge y)\wedge z\), (2) \(x\wedge y=y\wedge x\), (3) \(x\wedge x=x\), and (4) \(f_i(x\wedge y)\wedge f_i(y)=f_i(x\wedge y)\) -- for instance, the concept term \(A\sqcap\exists r_3.(X\sqcap B)\) is put into correspondence with the equation \(a\wedge f_3(x\wedge b)\); \item[{\(\bullet\)}] can be used to decide unification in the fragment of the modal logic \(\mathrm{K}_m\) that is restricted to the connectives \(\wedge\) and \(\lozenge_{r_i}\), by making concept names correspond to propositional variables, \(\sqcap\) to \(\wedge\), and \(\exists r_i\) to \(\lozenge_i\). \end{itemize}}