\cleardoublepage

\chapter{Should I Stay or Should I Go: A New Reasoner for Description Logic}\label{chap:emi}

\section{Introduction}
Knowledge graph schema are complex artifacts that can be very useful, but are often difficult and expensive to produce and maintain. This is especially true when encoding them in OWL (the Web Ontology Language) as ontologies for data management or reasoning. The high expressivity of OWL is a boon, in that it makes it possible to describe complex relationships between classes, roles,\footnote{We refer to properties as \textbf{roles}, unless a distinction is relevant, as this is the standard description logic term. These include both object properties and data properties.} and individuals in an ontology. At the same time, however, this high expressivity is often an obstacle to its correct usage that can limit adoption, and can hamper any practical reasoning applications by adding complexity to the reasoning process.

To manage the complexity of OWL some prefer to accept hardness as it is and develop tools to manage or simplify the tricky parts. However, it occasionally is the case that problems appear difficult when they are actually quite intuitive when expressed differently. When this happens it can be helpful to start again from the beginning and re-imagine what is possible by trying something entirely different. This will of course not alter the fundamental proven computational complexity of any reasoning or modeling problem. But it can lead to algorithms and design patterns that are more easily understandable, and potentially uncover unique use cases and optimizations.

In this spirit we have used a new API for OWL called (f OWL) \cite{fowl} for our experiment that can represent and better facilitate ontology data for the reasoning tasks we want it to perform. A custom reasoning algorithm called Emilia\footnote{\textbf{E}ager \textbf{M}aterializing and \textbf{I}terating \textbf{L}ogical \textbf{I}nference \textbf{A}lgorithm} (Emi) was implemented specifically to leverage the unique advantages of the new API, and with time the two will be able to seamlessly work within a single framework. The Emi reasoner will be able solve all of the same problems that current reasoners are able to solve, but its execution follows an iterative rule-like path rather than recursive tableau. 

This type of experiment may seem equivalent and redundant to logicians and mathematicians, and looking at it only in a purely formal sense this can seem to be the case, however Emi works entirely differently from current systems and presents many opportunities for new research. The reasoner presented here is a prototype which demonstrates that the technique is valid and no less efficient than other comparable Java Virtual Machine (JVM) reasoners -- the potential for new unique research directions and optimization techniques using this method will be the subject of future works. Initial testing is underway of Emi, and it is already performing competitively with other state-of-the-art systems in use today, and is particularly efficient with instance retrieval, despite being a naive prototype system written in a high level language with only the most basic and straightforward of optimizations.

\section{\texorpdfstring{\ALCH}{ALCH}}\label{subsubsec:ALC}
The Emi algorithm currently supports \ALCH\ reasoning, and the syntax and semantics of that logic are given below. Future extensions will likely expand expressivity for additional description logics.

\subsection{Syntax}
The signature $\Sigma$ for the Description Logic \ALCH\ is defined as $\Sigma = \left<N_I,N_C,N_R\right>\ $ where:

\begin{itemize}
\item $N_I$ is a set of individual element names.
\item $N_C$ is a set of class names that includes $\top$ and $\bot$.
\item $N_R$ is a set of role names.
\item $N_I, N_C, N_R$ are pairwise disjoint
\end{itemize}

\noindent Expressions in \ALCH\ use the following grammar:
\def\arraystretch{1.15}
\begin{table}%[H]
\centering
\begin{tabular}{lcl}
	$\textbf{R}$&$::=$&$N_R$\\
	$ \textbf{C} $&$::=$&$ N_C \ | \ \neg \textbf{C} \ | \ \textbf{C} \sqcap \textbf{C} \ | \ \textbf{C} \sqcup \textbf{C} \  | \ \exists \textbf{R}.\textbf{C} \ | \ \forall \textbf{R}.\textbf{C}$\\
\end{tabular}
\end{table}
\def\arraystretch{1}

\subsection{Semantics}
An interpretation $\mathcal{I} = \left( \Delta^\mathcal{I}, \cdot^\mathcal{I} \right)$ maps $N_I, \ N_C, \ N_R$ to elements, sets, and relations in $\Delta^\mathcal{I}$ with function $\cdot^\mathcal{I}$. An axiom $A$ in \ALCH\ is satisfiable if there is an interpretation where $\cdot^{\mathcal{I}}$ maps all elements, sets, and relations in $A$ to $\DeltaI$. An ontology $O$ is a set of axioms formed from \ALCH\ expressions, and is satisfiable if there is an interpretation that satisfies all axioms it contains, this interpretation being a model for $O$. $\cdot^{\mathcal{I}}$ is defined in Table 1 below.

\def\arraystretch{1.25}
\begin{table}%[H]
\centering
\caption{\ALCH\ Semantics}
\begin{tabular}{ c|c|c }
	\multicolumn{1}{c}{Description}&\multicolumn{1}{c}{Expression}&\multicolumn{1}{c}{Semantics}\\
\hline 
	Individual & $ x $ & $ x^{\mathcal{I}} \in \Delta^{\mathcal{I}} $\\    
    Top & $ \top $ & $ \Delta^{\mathcal{I}} $ \\ 
	Bottom & $ \bot $ & $ \emptyset $ \\
	Class & $ B $ & $ B^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}} $ \\
    Role & $ R $ & $ R^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}} \times \Delta^{\mathcal{I}} $ \\
    \hline
    Negation & $ \neg B $ & $ \Delta^I \setminus B^{\mathcal{I}} $ \\
    Conjunction & $ B \sqcap C $ & $ B^{\mathcal{I}} \cap C^{\mathcal{I}} $ \\
    Disjunction & $ B \sqcup C $ & $ B^{\mathcal{I}} \cup C^{\mathcal{I}} $ \\
    Existential Restriction & $ \exists R.B $ & \{ $ x \ | \ $there is $y \in \Delta^{\mathcal{I}}$ such that $ \left( x,y \right) \in R^{\mathcal{I}}$ and $y \in B^{\mathcal{I}} $ \} \\
    Universal Restriction & $ \forall R.B $ & \{ $ x \ | \ $ for all $y \in \Delta^{\mathcal{I}}$ where $ \left( x,y \right) \in R^{\mathcal{I}}$, we have $y \in B^{\mathcal{I}} $ \}\\
    \hline
    Class Assertion&$B(a)$&$\interpI{a} \in \interpI{B}$\\
    Role Assertion&$R(a,b)$&$(a,b) \in \interpI{R}$\\
    Negated Role Assertion&$\neg R(a,b)$&$(a,b) \not\in \interpI{R}$\\
    Class Subsumption& $B \sqsubseteq C$& $ B^{\mathcal{I}} \subseteq C^{\mathcal{I}}$\\
    Class Equivalence& $B \equiv C$ & $ B^{\mathcal{I}} = C^{\mathcal{I}}$\\
    Role Subsumption& $R \sqsubseteq S$& $ R^{\mathcal{I}} \subseteq S^{\mathcal{I}}$\\
\end{tabular}
\end{table}
\def\arraystretch{1}

\section{\fowl}
We use \fowl \cite{fowl} because it includes many novel optimizations that streamline ontology and reasoner development. True to the functional paradigm \fowl\ uses functions and shuns classes. Indeed all OWL ontology objects can be created directly with \fowl\ functions. And since these functions are not bound up in an arbitrary class hierarchy, they can operate on independent data structures that are internally typed to represent OWL semantics. A \fowl\ ontology itself is simply another data structure made of collections of smaller similar structures. This means that in most cases an expression, an axiom, even an ontology can be traversed recursively as-is without writing more functions. The use of immutable data structures by \fowl\ in standard Clojure style also permits straightforward implementation of concurrent processes that operate on ontology data.


\subsection{(f OWL) and Emi}
Emi makes use of many features of \fowl, some of which are uniquely advantageous in that they have no comparable alternative in other reasoners or APIs. One major advantage with using \fowl\ is the ontology-as-data-structure approach, which means that once \fowl\ has loaded the ontology into memory, Emi can efficiently traverse and manipulate expressions in the ontology without worrying about concurrency, since a \fowl\ ontology is immutable. Once the ontology is processed and elements in the signature are assigned mutable memory for use during reasoning, it is straightforward to define a partially paralellizable reasoning process with Clojure built-in functions that can be precisely lazy or eager when needed. The optimal configuration for when to choose each strategy is subject to many design trade-offs and does not have an objective best answer, though we believe we have developed a decent strategy. Emi processes axioms eagerly, but sets of axioms lazily and in parallel when possible due to the general observation that many non-synthetic ontologies contain a large number of axioms, most of which are rather small. This can affect performance on synthetic datasets where the occurrence of large or complex axioms is potentially higher and a different strategy may work better.

\section{Emi Reasoner}
As mentioned in the introduction, the new reasoner we are developing works iteratively without a graph, and is more like reasoning in \ELpp\ or datalog where the process runs on a loop that eventually terminates rather than an expansive graph traversal. %, even while solving problems in \ALCH. 
To reason iteratively we effectively need to turn the tableau inside out so we can work directly with axioms instead of a graph of elements. This means we will need to look at each axiom individually and add elements to or remove elements from expressions according to the tableau expansion rules as if they were backwards. This process slowly builds up a model for the ontology by partially realizing expressions until they become satisfiable and no longer need to be modified. Since every element is inspected for every axiom and the inverted tableau rules are followed in expressions we know this will be consistent. We assume that all expressions in our algorithm will be converted into Negation Normal Form (NNF); it is important to emphasize that absolutely no other logical preprocessing is used in the algorithm. In this section we assume that readers are familiar with the basics of tableau reasoning, if not they can consult \cite{baader2003description} for further information.

\subsection{Partial Interpretations}\label{subsec:exel}
This algorithm works by directly attempting to realize an ontology and eventually build a consistent interpretation using the axioms as they are written in NNF, by adding and removing elements until all axioms are satisfiable or the ontology is shown to be unsatisfiable. We refer to the changing states of a program as partial interpretations. 

Before continuing to the definition, it is important to stop and emphasize the subtle difference between partial interpretations and standard interpretations. A partial interpretation \emph{may} be equivalent to some interpretation, and indeed when Emi terminates and determines we have a satisfiable ontology this final partial interpretation is a model. However partial interpretations are not necessarily models and represent the states of the program as different assignments are attempted in order to find a model. This difference may be confusing at first for logicians who are used to only seeing standard interpretations, but the distinction is important not just for showing a simple proof but also for describing the actual implementation of the algorithm as well. Our terminology deliberately corresponds much more closely to how an actual implemented algorithm, rather than a theoretical proof of one, would function by avoiding whenever possible notions of infinity or concepts that would need to be represented by global variables that are pervasive in proofs and inconvenient or impossible to implement. We do this intentionally so that it can be understood by programmers as well as logicians; we hope not just to show correctness but that it is clear to anyone how they could actually write a reasoner such as this.
\begin{definition}
A \emph{partial interpretation} representing the current state of the algorithm when a function is called is $\is = (\mathcal{R}^\is,\cdot^\is)$ where $\cdot^\is$ is a function that maps elements, sets, and relations in an ontology $O$ to a realization $\mathcal{R}^\is$ of $O$.
\end{definition}
\begin{definition}
A \emph{realization} of ontology $O$ is a set of assertions that states for every class name $A$ and element $x$ in $O$ that $x \in A^\is$ or $x \not\in A^\is$ and for every role name $R$ and element pair $(x,y)$ in $O$ that $(x,y) \in R^\is$ or $(x,y) \not\in R^\is$.
\end{definition}
Each partial interpretation in this algorithm corresponds to some realization with a function $\cdot^\is$. Note that there is no restriction against inconsistent realizations and partial interpretations, only that they must be complete. A partial interpretation $\is$ with realization $\mathcal{R}^\is$ of ontology $O$ is said to be a model of $O$ iff there is an interpretation $\mathcal{I}$ of $O \cup \mathcal{R}^\is$.

As mentioned previously, while $\mathcal{I}$ often denotes a single consistent interpretation, $\is$ denotes the \emph{current interpretation} when a function is evaluated in the algorithm, and as such may change over time and contain information that is later proved to be incorrect. Frequently we will say things like ``Add $x$ to $E^\is$", and this indicates that the partial interpretation $\is$ will henceforth be modified in the program state to represent the described change to $\cdot^\is$ that produces the desired realization.

\subsection{Inverted Tableau Expansion Rules}
Inverting the tableau rules is straightforward when we turn the standard tableau terminology, such as occurs in \cite{baader2003description,10.5555/2890046.2890052}, on its head and assume that ``labels'' represent the action of the $\cdot^\is$ function on class and role names in an ontology to produce a realization, and that for any class or role name $E$ that $E^\is = \mathcal{L}(E)$. To connect this idea with labelling terminology in a graph we use a labelled object, which can represent both notions. 
\begin{definition}
A \emph{labelled object} $E$ is an object that is associated with some set $\mathcal{L}(E)$, or \emph{label}.
\end{definition}

First we note that nodes and labels do not necessarily need to be connected in a graph to represent the semantics of \ALCH, and can be reinterpreted as freely associating labelled objects. A labelled object can be a node in a tableau graph or simply an isolated named object with no inherent graph connections. This means that a label for a complex expression can be defined recursively to match the semantics of a partial interpretation $\is$, e.g. when an expression $C \sqcup D$ is satisfiable after applying the inverted tableau rules we have $\mathcal{L}(C \sqcup D) = (C \sqcup D)^\is = C^\is \cup D^\is$. We can represent axioms equivalently as labelled objects without actually needing to make a graph as long as all names in the signature are not duplicated in expressions but actually reference the same labelled objects. 

For this algorithm we consider the inverted \ALC\ tableau rules sufficient for deciding \ALCH\ satisfiability, since the addition of the $\mathcal{H}$ fragment does not permit complex role expressions and they do not require expansion to check. The RBox axioms that are not included here will be described in Table \ref{tab:alcosat} with the TBox axioms. In Table \ref{tab:tab} we show the tableau expansion rules for \ALC\ \cite{baader2003description} and assume the standard notion of blocking for them, which can be found with the original proofs, then show the inversions in Table \ref{tab:inv} where blocking is defined in Subsection \ref{subsec:Local Blocking}.

\begin{table}[H]
\centering
\begin{tabular}{l r l}
&&the following expansion rules apply to element $x$ when $x$ is not blocked\\
$\sqcap$-rule&if 1.&$(C \sqcap D) \in \mathcal{L}(x)$\\
&2.&$\{C,D\} \not\in \mathcal{L}(x)$\\
&then&$\mathcal{L}(x) \to \mathcal{L}(x) \cup \{C,D\}$\\

$\sqcup$-rule&if 1.&$(C \sqcup D) \in \mathcal{L}(x)$\\
&2.&$\{C,D\} \cap \mathcal{L}(x) = \emptyset$\\
&then&either $\mathcal{L}(x) \to \mathcal{L}(x) \cup \{C\}$\\
&&or else $\mathcal{L}(x) \to \mathcal{L}(x) \cup \{D\}$\\

$\exists$-rule&if 1.&$\exists R.C \in \mathcal{L}(x)$\\
&2.&there is no $y$ s.t. $\mathcal{L}((x,y)) = R$ and $C \in \mathcal{L}(x)$\\
&then&create a new node $y$ and edge $(x,y)$ with $\mathcal{L}(y) = \{C\}$ and $\mathcal{L}((x,y)) = R$\\

$\forall$-rule&if 1.&$\forall R.C \in \mathcal{L}(x)$\\
&2.&there is some $y$ s.t. $\mathcal{L}((x,y)) = R$ and $C \not\in \mathcal{L}(x)$\\
&then&$\mathcal{L}(y) \to \mathcal{L}(y) \cup \{C\}$\\
\end{tabular}%
\caption{\ALC\ Tableau Expansion Rules}\label{tab:tab}
\end{table}

\begin{table}%[H]
\centering
\begin{tabular}{l r l}
$\sqcap$-rule&if 1.&$x \in \mathcal{L}(C \sqcap D)$\\
&2.&$x \not\in \mathcal{L}(C) \cap \mathcal{L}(D)$\\
&then&$\mathcal{L}(C) \to \mathcal{L}(C) \cup \{x\}$\\
&&$\mathcal{L}(D) \to \mathcal{L}(D) \cup \{x\}$\\

$\sqcup$-rule&if 1.&$x \in \mathcal{L}(C \sqcup D)$\\
&2.&$x \not\in \mathcal{L}(C) \cup \mathcal{L}(D)$\\
&then&either $\mathcal{L}(C) \to \mathcal{L}(C) \cup \{x\}$\\
&&or else $\mathcal{L}(D) \to \mathcal{L}(D) \cup \{x\}$\\

$\exists$-rule&if 1.&$x \in \mathcal{L}(\exists R.C)$\\
&2.&there is no $y$ s.t. $(x,y) \in \mathcal{L}(R)$ and $y \in \mathcal{L}(C)$\\
&3.&there is no $z$ s.t. $x$ is blocked by $z$\\
&then&create a new element $y$ with $y \in \mathcal{L}(C)$ and $(x,y) \in \mathcal{L}(R)$\\

$\forall$-rule&if 1.&$x \in \mathcal{L}(\forall R.C)$\\
&2.&there is some $y$ s.t. $(x,y) \in \mathcal{L}(R)$ and $y \not\in \mathcal{L}(C)$\\
&then&$\mathcal{L}(C) \to \mathcal{L}(C) \cup \{x\}$\\
\end{tabular}%
\caption{Inverted \ALC\ Tableau Expansion Rules}\label{tab:inv}
\end{table}

The labelling terminology is used in this subsection to show tableau correspondence, though in general we avoid it since it is more obvious what is happening to non-logicians when we show our algorithm as an implementable process that produces interpretations, rather than a convoluted mathematical abstraction. Specifically, we believe it is more natural to think of a predicate that represents a set as a labelled object where the label represents the set associated with the predicate, than it is to invert this and represent all the elements as labels for connected sets of predicate names.

\subsection{ABox Expansion}
One of the more useful optimizations that this algorithm permits is the expansion of ABox axioms into many additional, unstated, expressions which must hold in every possible model. This expansion begins while the algorithm evaluates the ABox and detects any immediate clashes. Later while evaluating the TBox the expansion detects any clashes that cannot possibly be fixed to allow the algorithm to terminate quickly, and it can be done concurrently whenever the algorithm adds or removes elements from expressions. In Definition \ref{def:must} we maintain the assumption that all expressions are NNF and use $\neg$ to simplify the appearance of equivalent expressions.
\begin{definition}\label{def:must}
For partial interpretation $\is$, expression $E$, and element/pair $x$:
\begin{enumerate}
    \item A \emph{clash} means $x \in E^\is$ and $x \in \neg E^\is$
    \item $x$ \emph{must be in} $E$ iff there is no $\is$ where modifying $\cdot^\is$ to obtain $x \in \neg E^\is$ does not cause a clash
    \item $x$ \emph{must not be in} $E$ iff there is no $\is$ where modifying $\cdot^\is$ to obtain $x \in E^\is$ does not cause a clash
    \item An \emph{unresolvable clash} means $x$ must be in $E^\is$ and $x$ must not be in $E^\is$%$x \in E^\is_m$ and $x \in E_{\overline{m}}^\is$
\end{enumerate}
\end{definition}

The set of all elements that must be in an expression $E^\is$, denoted \mbis{E^\is}, is a subset of the elements of $E^\is$, and the set of all elements that must not be in $E^\is$, written \mnbis{E^\is}, is a subset of the elements of $\neg E^\is$. Like the expressions themselves, the exact members of \mbis{E^\is} and \mnbis{E^\is} are unknown at the beginning of the algorithm, so \mbis{E^\is} and \mnbis{E^\is} indicate the additional knowledge of constraints on satisfiability that grow as the algorithm runs and are thus referred to with the $\is$ as well. When we talk about element(s) being ``added" to these sets (nothing is ever removed), it is to indicate the change in $\cdot^\is$ that must hold in all future $\is$. Sets of elements that must (not) be in a complex expression can be computed in a straightforward way from the components of the expression they are in, for example $(B \sqcap C)_m^\is \equiv B_m^\is \sqcap C_m^\is$ and $(B \sqcap C)_{\overline{m}}^\is \equiv B^\is_{\overline{m}} \sqcup C^\is_{\overline{m}}$ (note the use of DeMorgan for $\overline{m}$).

Expansion occurs during TBox evaluation by, whenever possible, propagating the elements that must (not) be in expressions from antecedent to consequent, e.g. if we have axioms $\{A(x),A \sqsubseteq B\}$ then $x \in A_m$, and when we check $A \sqsubseteq B$ it is often possible to conclude $x \in B_m$. This is not always possible for expressions containing disjunction and negation except in certain very specific cases. Regardless the effect is powerful. Maintaining these sets allows us to explore only potentially correct solutions by preemptively avoiding actions that will be inconsistent in every model and also detect unresolvable clashes so the evaluation can terminate more quickly.

\subsection{Local Blocking}\label{subsec:Local Blocking}
The notion of blocking is also required for termination due to the new elements\footnote{When we say `new element' this is equivalent to a fresh element symbol. It is written this way because we are avoiding terminology that refers to an infinite set of names and instead refer to what a program really does here, i.e. create something new} created by the existential function. Our notion of blocking corresponds to the usual definition in that it references the same cyclic patterns in roles, however Emi cannot use blocking in reference to the global role hierarchy which is not computed explicitly, so cycles are detected locally by tracing the dependency paths that emerge as new elements are created to satisfy expressions.

\begin{definition}
A new element $x$ was \emph{created to satisfy} expression $\exists R.B$ in an algorithm $A$ if there are partial interpretations $\is,\is'$ for $A$ where for some $y$ we have $(y,x) \in R^\is, x \in B^\is, y \in \exists R.B^{\is}$ and $y \not\in \exists R.B^{\is'}$ if $x \not\in \Delta^{\is'}$.
\end{definition}
\begin{definition}
For expression $\exists R.B^\is$, an element $x$ is \emph{blocked} by element $z$ if $(z,x) \in R^\is$ and $x$ was created to satisfy $\exists R.B$, or if for $(z,y_0) \in R^\is$ where $y_0$ was created to satisfy $\exists R.B$ we have $n \geq 0$ pairs of elements such that $\bigcup_{k = 1}^n (y_{k-1},y_k) \cup \{ (y_n,x) \} \subseteq \Delta^\is \times \Delta^\is$.
\end{definition}
Fortunately this restriction is rather intuitive to implement: we simply need the function for an existential to not create new elements when checking new elements that exist as a result of a prior application of the same function on the same existential, since this will induce a cycle. It is effectively as if elements have a `history' represented by the chain of pairs that they inherit from the element that created them and which also contains their own origin. An element will therefore not generate new elements in a function with the existential that created it, and not if the function for the existential created an element that it depends on for its existence, or that is in its `history'.

\subsection{Termination Condition}\label{subsec:term}
The final component necessary for the algorithm to work is a termination condition. Unlike a tableau, this algorithm will run on a loop and will actually attempt to directly realize the ontology. How then do we know that the algorithm has correctly realized all of the axioms? This is actually rather simple. If the algorithm begins an iteration of checking all axioms with initial state $\mathcal{I}^*_a$ and ends this iteration with state $\mathcal{I}^*_b$ without encountering any unresolvable clashes, then we know it can terminate successfully if $\mathcal{I}^*_a = \mathcal{I}^*_b$. Since we know that each $\is$ represents a possible interpretation, it is clear that $\is$ is a model when no clash occurs after every axiom is checked and all elements remain the same in all expressions.
\begin{definition}
A partial interpretation $\is$ is said to \emph{equal} partial interpretation $\is'$, or $\is = \is'$, iff $\forall E \in N_C \cup N_R$ we have $E^{\is} = E^{\is'}$.
\end{definition}
Equality can be verified by checking if the names in the signature have not changed any of their memberships. If an element has been added to the signature, or has moved into or out of any class or role, the algorithm must check the axioms one more time to see if these changes cause side effects. Otherwise the algorithm will have checked every axiom and found them to be satisfiable without making any changes and has produced a model.

\subsection{Algorithm Definition}
An outline of Emi is shown in Algorithm \ref{alg:sat} that uses functions from Table \ref{tab:alcosat}. 

\subsubsection{Backtracking}
Explicit backtracking in this algorithm is handled by `reporting' clashes and unresolvable clashes.
\begin{definition}
A \emph{report} for Algorithm \ref{alg:emi} immediately terminates execution of whatever process is occurring and returns to the function that handles this report.
\end{definition}
A report is meant to act like a programming exception. For example, when an unresolvable clash is directly reported while evaluating the ABox the behavior is clear, the ontology is unsatisfiable so all reasoning stops and the algorithm immediately exits by returning False. 

Standard clashes occur when the inverted tableau rules require an action that is known to be inconsistent, but which could potentially be resolved by making changes elsewhere. In this case the immediate action is to stop trying the obviously inconsistent task and instead do something different. This type of clash is normally handled in Emi by the code that solves the inverted tableau rules in the same way that a standard tableau might. However, there are cases where the $sat$ function must intervene, for instance when the antecedent of an axiom can neither lack nor contain an element and both assignments have been attempted to exhaustion. In this case we have indirectly found an unresolvable clash. If a clash is reported but is able to be resolved, the algorithm merely proceeds along as normal, and any problems that a removal causes will themselves be reported and dealt with in the same way. Emi internally ensures that backtracking does not return to an identical previous program state so that termination is not a concern. ABox expansion greatly impacts this functionality by automatically removing many impossible solutions from consideration, allowing these reports to happen faster.

\subsubsection{Parallelization}
\def\arraystretch{1.2}
\begin{table}%[H]
\centering
\caption{$sat$ function behavior for \ALCH\ satisfiability of ontology $O$, class name $A$, class expressions $B,C$, and roles $R,S$}\label{tab:alcosat}
\begin{tabular}{l l}
Axiom&Action\\
\hline
$A(a)$&$\text{If }\inmnbis{A}{a}\text{ report an unresolvable clash, otherwise add }a\text{ to }A^\is\text{ and \mbis{A^\is}}$\\
$\neg A(a)$&$\text{If }\inmbis{A}{a}\text{ report an unresolvable clash, otherwise add }a\text{ to \mnbis{A^\is}}$\\
$B(a)$&$\text{Add a new class } A \text{ and the axiom }A \sqsubseteq B\text{ to }O\text{ and replace }B(a) \text{ with }A(a)$\\
$R(a,b)$&If $\inmnbis{R}{(a,b)}$ report an unresolvable clash, otherwise add $(a,b)$ to $R^\is$ and \mbis{R^\is}\\
$\neg R(a,b)$&If $\inmbis{R}{(a,b)}$ report an unresolvable clash, otherwise add $(a,b)$ to \mnbis{R^\is}\\
\hline
\multirow{3}{*}{$B \sqsubseteq C$}&For all $x \in B^\is$ add $x$ to $C$ using the inverted tableau expansion rules.\\
&If a clash is reported, instead bactrack to remove $x$ from $B$.\\
&If both report a clash, report an unresolvable clash.\\
$B \equiv C$&Do $sat(B \sqsubseteq C)$ and $sat(C \sqsubseteq B)$ and report any unresolvable clashes.\\
\hline
\multirow{2}{*}{$R \sqsubseteq S$}&For all $(x,y) \in R^\is$ add $(x,y)$ to $S$. If a clash is reported, instead backtrack to\\
&remove $(x,y)$ from $R$. If both report a clash, report an unresolvable clash.\\
\end{tabular}%
\end{table}
\def\arraystretch{1}

Because we are not working with one single expanded concept representing the entire set of axioms like a standard tableau, it is possible in this algorithm to parallelize many operations on separate axioms. In the simplest case, it is unproblematic for the algorithm to process more than one axiom at the same time so long as they do not share any class or role names. Clashes that occur as a result of two independent axioms will in either case still be detected elsewhere and are dealt with regardless of the ordering. Additionally, this idea can be extended in the implementation to allow for axioms that share names to be evaluated concurrently as well, so long as shared names are not modified in ways that can cause a clash and begin backtracking. Emi makes use of the simplest case already and the implementation of more complex parallelization is in development.

\begin{algorithm}[H]
\label{alg:emi}
\SetAlgoNoLine
\SetKwRepeat{DoWhile}{do}{while}
\caption{\ALCH\ satisfiability for ontology $O$}\label{alg:sat}
\KwResult{A realization that is a model of $O$ when $True$, otherwise $False$ when an unresolvable clash occurs}
\BlankLine
\tcp{Initialize an empty set to represent a realization for $O$}
$\is \gets \{\}$\;
\BlankLine
\tcp{Assume all $E/E_m/E_{\overline{m}}$ are empty and add them to $\is$}
\For{$E \in N_C \cup N_R$}{
$E \gets \{\}$;\\
$E_m \gets \{\}$;\\
$E_{\overline{m}}  \gets \{\}$;\\
$\is \gets \is \cup \{E,E_m,E_{\overline{m}}\}$\;
}\BlankLine
\tcp{Obtain NNF of all axioms}
$\mathcal{F} \gets$ NNF of ABox of $O$\;
$\mathcal{A} \gets$ NNF of TBox of $O$\;
\BlankLine
\tcp{Process ABox}
\For{$F \in \mathcal{F}$}{
 $sat(F)$\;\BlankLine
 \If{an unresolvable clash is reported}{\Return{False}}
}
\BlankLine
\tcp{Process TBox}
\Repeat{$\mathcal{I}^* = \mathcal{I}^*_{old}$}{
 $\mathcal{I}^*_{old} \gets \mathcal{I}^*$\;
 \BlankLine
 \For{$A \in \mathcal{A}$}{
  $sat(A)$\;
  \BlankLine  
  \If{an unresolvable clash is reported}{\Return{False}}
  \BlankLine
 }
}
\BlankLine
\Return{True}
\end{algorithm}



\subsection{Correctness}
The correctness of this algorithm follows from the direct correspondence between the tableau rules and their inversions along with a few minor details. First we will examine the inverted tableau rules. Each rule contains two distinct states in both the standard and inverted rules, the antecedent `if' clause where certain conditions must hold, and the consequent `then' clause where changes are made to the state in order to find a model. Thus it will be sufficient to show that each `if' and `then' clause from the inverted tableau rules is re-writable into the corresponding clause in the standard tableau rules.

\begin{enumerate}
\item[$\sqcap$-rule]
\item[]\begin{enumerate}
    \item[`if'] This state in the inverted tableau rules corresponds to the standard tableau rules, since in each case we know $x$ should be in $C \sqcap D$, but it is either not in $C$ or $D$ or both.
    \item[`then'] The change made in response to the `if' clause is also equivalent, since the inversion adding $x$ to $C^\is$ and $D^\is$ represents the notion that we now have $x \in C^\is$ and $x \in D^\is$ which is identical to the standard tableau rules adding $\{C,D\}$ to $\mathcal{L}(x)$.
\end{enumerate}

\item[$\sqcup$-rule]
\item[]\begin{enumerate}
    \item[`if'] This state in the inverted tableau rules corresponds to the standard tableau rules, since in each case we know $x$ should be in $C \sqcup D$, but it is neither in $C$ nor in $D$.
    \item[`then'] The change made in response to the `if' clause is also equivalent, since the inversion adding $x$ to $C^\is$ or $D^\is$ represents the notion that we now have $x \in C^\is$ or $x \in D^\is$ which is identical to the standard tableau rules either adding $\{C\}$ to $\mathcal{L}(x)$ or adding $\{D\}$ to $\mathcal{L}(x)$.
\end{enumerate}

\item[$\exists$-rule]
\item[]\begin{enumerate}
    \item[`if'] This state in the inverted tableau rules corresponds to the standard tableau rules, since in each case we know $x$ should be in $\exists R.C$, but the current state means that there is either no $(x,y) \in R$ such that $y \in C$ or there is no $y \in C$ such that $(x,y) \in R$. The blocking condition (3) only applies when $x$ is blocked because it is a new individual that exists as a (possibly indirect) result of an element previously created to satisfy this expression. When $x$ is blocked in this way it is clear that we have completed the first iteration of a cycle and do not need to continue.
    \item[`then'] The change made in response to the `if' clause is also equivalent, since the inversion creating some $y$ such that $y \in C^\is$ and $(x,y) \in R^\is$ represents the notion that $x \in \exists R.C$, which is identical to the standard tableau rules creating a new node and edge for $y$ with $\mathcal{L}(y) = \{C\}$ and $\mathcal{L}((x,y)) = R$.
\end{enumerate}

\item[$\forall$-rule]
\item[]\begin{enumerate}
    \item[`if'] This state in the inverted tableau rules corresponds to the standard tableau rules, since in each case we know $x$ should be in $\forall R.C$, but the current state means that there is some $y$ such that $(x,y) \in R$ and $y \not\in C$.
    \item[`then'] The change made in response to the `if' clause is also equivalent, since the inversion adding every $y$ to $C^\is$ wherever $(x,y) \in R^\is$ represents the notion that $x \in \forall R.C$, which is identical to the standard tableau rules adding $\{C\}$ to any $y$ so that $\mathcal{L}(y) = \{C\}$.
\end{enumerate}
\end{enumerate}


The only remaining thing to discuss is that Algorithm \ref{alg:emi} and the $sat$ function are sound and complete. For this it is simple to outline without a lengthy proof, since as we mentioned previously, the sat functions will test all elements in all expressions with the tableau expansion rules, exactly as you would have in a tableau. It is unnecessary and in fact unhelpful in this algorithm to combine all expressions into a connected whole since each axiom is itself evaluated consistently.

The subsumption axioms are solved in such a way that they implicitly compute a class and role hierarchy, so any inference dependent on a hierarchy will still be entailed. Next, the stop condition of Algorithm \ref{alg:emi} when the interpretation has not changed is identical with a completed tableau that no longer requires expansion or backtracking since both are models. And of course all cases where unresolvable clashes can occur are sound because they indicate instances where an element simultaneously must be in and must not be in an expression so the algorithm should terminate. As for completeness, it is again clear that whenever an unresolvable clash occurs it is identical with a case when a tableau discovers a clash but cannot backtrack to correct it.

\section{Evaluation}
The implementation of the Emi reasoner is evaluated against other popular JVM reasoners such as Hermit\footnote{Hermit Version 1.4.5.519}, Pellet\footnote{Openllet Version 2.6.5}, and jFact\footnote{jFact Version 5.0.3} \cite{10.1007/s10817-014-9305-1,10.1016/j.websem.2007.03.004,10.1007/11814771_26} using Leiningen\footnote{\url{https://leiningen.org/}}, which can run Clojure as well as Java programs. 500 ontologies were randomly sampled, half from ODPs and Biomedical ontologies in \cite{10.1007/978-3-030-77385-4_14}, and half from the Ontology Reasoner Evaluation 2015 competition dataset. These files were altered by removing any axiom that is not expressible in \ALCH\ for testing. Among the 500 ontologies, 56 of them either timed out on all reasoners or caused our evaluation program to crash in some unexpected way due to lack of heap. It is not entirely clear from our logs which reasoner may be breaking in this way so we omit them, though we are confident that Emi has no heap issues or memory leaks (it is quite difficult to even \emph{intentionally} create memory leaks with Clojure) and it can load all files by itself without error.

All testing was done on a computer running Ubuntu 20.04.1 64-bit with an Intel Core i7-9700K CPU@3.60GHz x 8, 47.1 GiB DDR4, and a GeForce GTX 1060 6GB/PCIe/SSE2.

\subsection{Results}
Testing and development is ongoing for the Emi reasoner and these results are a first example of the potential for this type of algorithm. A preliminary example of the reasoning time can be found in Figure \ref{fig:allTime}. In this example, 3 tests are performed and timed on each reasoner: initialization from a file in memory shown in Figure \ref{fig:initTime}, satisfiability and consistency checking shown in Figure \ref{fig:satTime}, and retrieval of the elements in all non-empty class and role names after reasoning has completed shown in Figure \ref{fig:nonMTTime}.\footnote{Raw data and charts are available for inspection \url{https://tinyurl.com/kgswc2023}} Each test was given a timeout of 5 minutes, and when a test timed out more than 5 tests in a row for a reasoner it was prevented from testing again on the same file to save time in the evaluation. Across all tests, when we compare the percent difference between the reasoner time and the average time for all reasoners we see that Emi is overall $9.8\%$ faster than average, Hermit is $4.2\%$ slower than average, Pellet is $42.3\%$ faster than average, and jFact is $55.9\%$ slower than average. No reasoner was ever more than 100\% better than average or 300\% worse than average. Emi, Hermit, and Pellet each had 2 files when they failed due to an exception, while jFact failed on 70 files, though this is largely due to an issue it has with anonymous individuals in the ORE dataset.

As you can see in Figures 2 and 3, the Emi reasoner has a relatively slow initialize time and time for satisfiability on small ontologies. This is partially due to the fact that Emi solves all ABox axioms without complex expressions while it loads the ontology. This allows it to preemptively reject any naively unsatisfiable ABox, and the cost of this is usually only a few milliseconds. Emi seems to scale better than other systems and its performance improves in comparison as the number of axioms increases. Also, Emi is definitively faster in every single test when asked to compute the elements of all non-empty classes and roles, except the two tests where it had a timeout when computing satisfiability. Emi finishes reasoning with this information already computed, it is in effect computing both things at once, and only needs a variable amount of time to answer in our tests because it has to sort out the anonymous elements from every expression for comparison with the other reasoners where these elements are hidden by the OWL API \cite{10.5555/2890046.2890052}. Otherwise it could answer this in constant time.

Looking more closely at the data, there are three large clusters at 163, 325, and approximately 5500 axioms due to the synthetic ontologies in the ORE dataset. As you can see, all reasoners appear to behave similarly across multiple files of the same size in the clusters. Except for these clusters there appears to be a mostly stochastic distribution in the performance of each reasoner across different files with jFact doing great on small files but not scaling well, while Hermit, Pellet, and Emi start off a bit slower and seem to scale much better on very large files.

An interesting pattern we have noticed in the evaluation is that Emi usually outperforms other reasoners when it checks large ontologies with empty or nearly-empty ABoxes. This case makes sense when you notice that in $\mathcal{ALCH}$, as long as all axioms do not contain either negation or Top in the antecedent, there will always be a model where every predicate is empty. This is the default state when Emi starts, so it simply checks everything and the initial realization turns out to be fine after the first iteration.

\begin{figure}%[t]
\centering
\begin{minipage}{0.45\textwidth}
\centering
\includegraphics[width=\textwidth*9/10]{figures/allTime.pdf}
\caption{All Reasoning Tests}
\label{fig:allTime}
\end{minipage}
\begin{minipage}{0.45\textwidth}%[t]
\centering
\includegraphics[width=\textwidth*9/10]{figures/initTime.pdf}
\caption{Initialize}
\label{fig:initTime}
\end{minipage}
\end{figure}

\begin{figure}%[t]
\centering
\begin{minipage}{0.45\textwidth}
\centering
\includegraphics[width=\textwidth*9/10]{figures/satTime.pdf}
\caption{Satisfiability}
\label{fig:satTime}
\end{minipage}
\begin{minipage}{0.45\textwidth}
\centering
\includegraphics[width=\textwidth*9/10]{figures/nonMTTime.pdf}
\caption{Non-Empty Classes and Roles}
\label{fig:nonMTTime}
\end{minipage}
\end{figure}

\section{Future Work}
In the future there is quite a bit of work left to finalize and sufficiently verify Emi. These improvements will be ongoing as part of any new extensions. Parallelization in particular will likely prove difficult to formally pin down, though empirically its use is not as yet seeming to be problematic when comparing against the behavior of other reasoners. Some obvious extensions that are planned for the near future are inverse roles, nominals, and cardinality expressions which can work quite directly with some of the already existing code. Role chains are another interesting and useful addition we are considering, though these will be difficult to implement efficiently so we will be cautious.

An interesting observation we have made while considering extensions is that some of the common difficulty with nominals in reasoning may turn out to be trivial in many cases for the Emi algorithm because nominals are not necessarily connected to anything as long as we maintain sufficient information about (in)equality. Once this is implemented and our hypothesis is checked it would also be straightforward to extend nominals to nominal schemas, since Emi does not normalize or pre-process away the original axioms. Initial testing suggest there is an intuitive way to bind nominal variables within axioms to solve this directly as Emi reasons.
