\chapter{Cwm Reasoner}
\section{Introduction}
First written in October 2000, Cwm is a tool to explore the Semantic Web language syntax and reasoning. Cwm can read data in RDF/XML and Notation3 formats, and output in both also. It is often used simply to convert formats. It can merge documents into a larger one. Cwm understands a rule language written in Notation3, and can process those rules. 


\section{Forward Chained Reasoner}
Perhaps the largest single part of Cwm is the forward chaining reasoner. Given rules written using \qname{log:implies}\footnote{The \qname{log} namespace stands for the URI \uri{http://www.w3.org/2000/10/swap/log#}, so this is the URI \uri{http://www.w3.org/2000/10/swap/log#implies}.}, the forward chainer tries to match every rule, trying to find more facts. It will keep doing this until there are no more facts to be found. It is quite possible for it to loop forever instead, so it that case it will do just that. In order to do more than pattern replacement, CWM supports builtins. It is possible for a rule triple to be created in running the rule engine. In that case, the rule is added to the set of rules and processing continues.

Forward chainers are straightforward to understand. Many types of rules engines use them.

A problem with forward chainers is that they can easily do a tremendous amount of useless work. Given RDFS and a rule
\begin{verbatim}
{?C1 rdfs:subClassOf ?C2 . 
?X a ?C1} => {?X a ?C2} .
\end{verbatim}
It can easily figure out that everything is a \qname{rdfs:Resource}, the universal class of RDFS. This is almost certainly a waste of work.

Of course, these rules engines can get into much worse trouble than that. Cwm allows for implying the existence of something, with the syntax:
\begin{verbatim}
{...} => {@forSome :A . ... } .
\end{verbatim}
The reasoner must assume that $:A$, as asserted there, is different from every other individual ever seen. Therefore, it becomes trivial to assert the existence of an infinite number of statements. 
\begin{verbatim}
{?X a :Man} 
=> 
{@forSome :A . ?X @has :father :A . :A a :Man}
\end{verbatim} 
The forward chainer will (correctly) run forever on this. 

It is not even possible for any reasoning strategy to detect all cases of infinite loops. By Appendix \ref{turing}, these rules are universal. It is impossible by the halting theorem to always detect if they will loop forever. Therefore, it is likely very useful in some instances of Notation3 rules to disallow these implied existentials. So long as one does not have them (or lists, or implied nested formulae), then the number of individuals is finite, and therefore the number of possible triples is finite. Therefore, it is trivial to show that the system must halt.

If we allow implying existentials, a na\"\i{}ve implementation would incorrectly loop forever. If given the following (trivial by RDF semantics) rule:
\begin{verbatim}
{?X a :Man} => {@forSome :A . :A a :Man} .
\end{verbatim}
it will loop forever creating an infinite number of statements, all saying essentially ``there exists a Man.'' By RDF semantics, every one of those statements is redundant. Because they are not adding anything, the reasoner should detect this and stop. Cwm is not perfect in this regard, but gets most cases correct. \footnote{See appendix \ref{skolem-vs-entailment} for an explanation of what Cwm does, and does not, do}


\subsection{Technique}
CWM very aggressively indexes its triples to make search easier. There are eight types of patterns, given that there can be variables in every spot of the triple. CWM puts a triple in eight indexes, one per pattern type, so that the set that needs to be searched is greatly reduced. 


\subsection{Builtins}
\label{builtin-cwm}
In order to implement builtin predicates, as described in section \ref{builtin-n3}, Cwm's matcher does a large amount of work. The issue is that one could write a graph that says:
\begin{verbatim}
(1 2) math:sum 35 .
\end{verbatim}

Cwm's matcher, at every stage, tries to find the easiest pattern triple to match. If a triple is a builtin that cannot be run yet, then by definition it cannot be the easiest pattern to match. Otherwise, the search uses the pattern with the smallest index. When it runs that, it generates all matches for that pattern, be they in the given statements or built in. For each match, it continues that search for the rest of the pattern triples.

This is a greedy \emph{dynamic ordering}. At every step, it does whatever looks easiest right now. This may not cause the globally easiest match, but the cost of a search is dominated by the early branching factor enough that it helps. 

\label{static-ordering}
Another thing that could be done is static ordering. By doing so, the reasoner would predetermine the order that it matches patterns to facts. The RETE algorithm\cite{reteul} as described in section \ref{rete-algorithm} does this, trading dynamic ordering for the ability to save partial matches. Now, however, matching a builtin is much harder. It must be recognized as a builtin, and put in a place low enough in the match that it can run, but high enough to be above anything that depends on it. So long as what is a builtin is clear, a topological sort would work. Nonetheless, this requires information Cwm does not have. Its builtins only answer if they can now run, not what they need to be able to run. 

\section{Backward Chained Reasoner}
The essence of backward chaining is to look starting from the answer needed to find the data needed to answer it. By doing this, in many problems much less work needs to be done than with a forward chainer, because much of the data can be ignored. However, depending on the queries generated, it may very well be that a backward chainer does more work.

Backward chaining runs into problems that do not exist in forward chaining. Indeed, the na\"\i{}ve way of implementing a backward chaining reasoner, as Prolog does it, has severe looping problems. 

As an example, we will look at a simple rule, that might appear in a ruleset for processing RDFS. The rule is 
\begin{verbatim}
{?x a ?C1 . ?C1 rdfs:subClassOf ?C2} => {?x a ?C2} .
\end{verbatim}
We note that running the Prolog rules on this rule, and a query \verb|:Bob a ?C|, generates the query \verb|:Bob a ?C1|. This is then run, generating the query \verb|:Bob a ?C1|. This is then run. We see that the reasoner is caught in a loop, trying to answer a query by running the same query again.

Prolog systems solve this problem by a combination of two factors. First, they are looking for a \emph{a} answer, not \emph{every} answer. Therefore, once one answer is found, it stops. It does not have to get into cases that may loop trying to find other answers. The other one is that the rules are ordered. By putting non looping rules before looping ones, it will avoid loops if possible. In combination, these two allow the programmer to avoid infinite loops.

We note that neither of these properties are true in Notation3 rules. A Notation3 graph is unordered, and therefore there is no way to order the rules. Further, this lack of order means that we do not know which answer we want. In truth, we want the system to returns every answer to a query.

The idea that Euler \cite{euler} uses is loop detection. At ever step of the query, it keeps a list of previous queries in the stack. If the current one is equivalent to a previous one, the query fails right there. In our example, at the point of the first \verb|:Bob a ?C1| query, it would detect the loop and fail, backtracking the search.

We note that there is still a great deal of redundant work possibly being done. In a single search tree, it is possible for the same query to come up again and again, so long as it is never from a descendant of another copy. 

The solution I preferred was tabling. Essentially, tabling builds a table of queries and their results. When running a query, the object associated with it is registered in the table. Any queries generated are first checked in the table. If they are not there, they are run. If they are there, a listener is installed for whenever they return a result. This stops those trivial loops.

As an example, let us look at the \verb|subClassOf| rule seen before. Starting from a query \verb|:Bob a ?C|, an query object for that is created and added to the table. At that point, the rule shown is selected. Two more queries are needed. The first, \verb|:Bob a ?C1|, is already in the table. Therefore, it installs the callback from that object. The other \verb|?C1 rdfs:subClassOf ?C2|, is then instantiated. In this way, the query process terminates.

The lack of negation as failure in this logic creates some good properties for this reasoner. While \cite{xsb} has a much more complex tabling algorithm to handle negation, we don't need any of it. The result is, that the algorithm is relatively straightforward. 

A backward chainer is not perfect. For instance, given a rule to support \verb|rdfs:subPropertyOf|, 
\begin{verbatim}
{?P1 rdfs:subPropertyOf ?P2 .
 ?S ?P1 ?O } => {?S ?P2 ?O} .
\end{verbatim}
It is possible for a query of \verb|?S ?P2 ?O| to be generated. This will cause a query for every statement to be generated, and remove all benefit from the backward chainer. The backward chainer will do all of the work of a forward chainer anyways.

It is a result of the halting theorem that no technique is perfect; there is no way to stop the reasoner from running forever on some inputs. Clearly, with a backward chainer some inputs require much less work. 

%% Compare tabling and look checking

The backward chaining reasoner also can compute results that the forward chainer will refuse to. One such example is \uri{http://www.w3.org/2000/10/swap/test/include/t10.n3}, which says in part:
\begin{verbatim}
{ :doc log:semantics :F .
  :F  log:includes :G } log:implies  {  :doc local:says :G }. 

{ <t10a.n3> local:says { :theSky :is :blue } } 
log:implies {:test_SURPRISE a :success}.
\end{verbatim}

The builtin system for Cwm will refuse to find the \qname{log:sematics} of a non-specified file, so it cannot run this. However, the backward chainer will note that it wants to know if \verb|:test_SURPRISE| is a \qname{:success}. This leads to the query if \verb|<t10a.n3> local:says { :theSky :is :blue }|. The query that is run for the builtin predicate is therefore \verb|<t10a.n3> log:semantics :F|, which it can run.

In order to implement the backward chaining, the indexes needed to be extended. A statement like \verb|@forAll :X . :X a rdfs:Resource| will match many ground queries. Because of this, any query triple will need to read from up to eight indexes instead of one. Each triple will still appear in eight indexes. For a ground triple, it will appear in the same eight. For a triple with a variable, the variable will be replaced by a generic variable placeholder before choosing indexes. Let us take an example. 

While there are very few top-level statements with variables, in a backward chainer, there are many statements with variables. The rule
\begin{verbatim}
{?X a ?C1 . ?C1 rdfs:subClassOf ?C2} => {?X a ?C2}
\end{verbatim}
generates the statement \verb|?X a ?C2|. There are two variables. This would
 appear in eight indexes. These are: \\
\begin{tabular}{ccc}
\verb|VAR| & \qname{rdf:type} \footnote{As noted in Appendix \ref{notation3-syntax}, $a$ stands for \qname{rdf:type}} & \verb|VAR| \\
None & \qname{rdf:type} & \verb|VAR| \\
\verb|VAR| & None & \verb|VAR| \\
\verb|VAR| & \qname{rdf:type} & None \\
None & None & \verb|VAR| \\
None & \qname{rdf:type} & None \\
\verb|VAR| & None & None \\
None & None & None 
\end{tabular}

The corresponding query \verb|?X a ?C2| would be querying from two index lists. It would be using \\
\begin{tabular}{ccc}
None & \qname{rdf:type} & None \\
None & \verb|VAR| & None
\end{tabular}

The variables must match \verb|None|, because they will match anything. Because \verb|VAR| also goes into \verb|None|, the subject and object with \verb|None| are redundant. A ground query will combine eight indexes. 

\section{SPARQL query engine}
A recent effort was to create a query engine for RDF data and the Semantic Web. The result was SPARQL\cite{sparql}, a standard query language for the Semantic Web. A SPARQL query is an instruction on what to return and a patterns or expression of patterns to match in one or more RDF graphs. 

It was noticed that a query engine is a piece of a rule engine. A SPARQL query looks a great deal like a Cwm rule. Adding SPARQL query support to Cwm was considered a useful feature. The question was how to implement that feature.

A typical SPARQL query may look like:
\begin{verbatim}
PREFIX : <http://example.com/#>
SELECT ?x
WHERE {?y :p1 ?x . ?x :p2 :Foo}
\end{verbatim}
This is very similar to the Notation3 rule:
\begin{verbatim}
{?y :p1 ?x . ?x :p2 :Foo} => {(?x) a sparql:Result} .
\end{verbatim}
This is why it was thought that the mapping would be natural.

At the time this implementation work was done (summer 2005), SPARQL was not yet a Recommendation. The section of the standard specifying how to process queries was not written yet. There was a great deal of freedom in how to implement the query engine. Given this, I tried to write a converter from SPARQL to Notation3 rules. Then the existing query engine could run the queries. 

\verb|OPTIONAL| in a sparql query allows for the optional matching of part of a graph. If the part inside of the optional section can match, then it must. Otherwise, the query can succeed without it. 

It quickly became clear that the translation was not as straightforward as first thought. The use of nested \verb|OPTIONAL| keyword blocks in a query starts to get some very unclear semantics, and does not map well to the Notation3 rules. Combinations of \verb|OPTIONAL|s and \verb|UNION|s were resulting in some weird interactions, that had some complex translations.

The \verb|FILTER| expressions caused bigger problems. A \verb|FILTER| is an algebraic expression that must be true for the match to succeed. Each function in a \verb|FILTER| expression has input types and output types. Which Notation3 builtin was mapped to would depend sometimes on the input types. Further, there were type coercions when the output type of one did not map to the input type of another. Sometimes, the result of an expression was a TypeError. This may have come up when compiling the \verb|FILTER| expression, or when running the query. Finally, TypeError is a value that is neither TRUE nor FALSE, and behaves oddly in Boolean logic.

The lack of support for OR in N3 rules became a problem. Splitting the query into two for every choice works when there are just \verb|UNION|s, and a few of them. But \uri{http://www.w3.org/2000/10/swap/test/sparql/union5.sparql} shows the exponential blowup. Further, this requires all ORs to be at the top level. The rules for distributing OPTIONALs and ANDs over ORs are in fact not always possible in the presence of TypeError. 

In order to talk about parsing, let us talk about parsers and grammars. The power of the machine needed to recognize a language is its expressivity. Typically, parsing is done by a context free grammar, modeling a nondeterministic stack machine. Given that our computer are deterministic, emulating this on a computer is not always trivial. Therefore, subsets of the class of all context free grammars are used.

A bottom up parser builds up states from the bottom up. Things tend to associate from right to left. These are known as LR(k) parsers. A top-down parser does the opposite, and is known as a LL(k) parser. 

In both of these parsers, the (k) determines the number of tokens the parser remembers at once to figure out the state. The lowest numbers, and most commonly appearing, are LL(0), which saves one character, and LALR(1), which is not a full LR(1). A nondeterministic parser would not work with any finite $k$. 

It is important to note that people do not write LR parsers. Rather, people write code that is compiled into the LR parser. The actual parser is a table 

The first step in the process was the building of a grammar. The grammar provided in the SPARQL standard was not sufficient. It was designed for a LALR(1) parser, while the parser engine I had was a LL(0) parser. I figured out how to modify the grammar to have the correct expressivity. The resulting grammar is, unfortunately, much less straightforward. 

Once it is done parsing, a parse tree is generated. This is converted in a bottom-up manner into the Notation3 rules. However, as we have seen, this conversion is far from being straightforward. 


\section{Proof Generation and Checking}
For any sort of problem solving, there is the distinction between solution finding and solution checking. If one finds a solution, then one can go through the steps one went through to find the solution and print them out. Given these, verifying that a solution was indeed given is linear in the length of the step list (so long as each step is constant time). This is while there may be no bound whatsoever on the amount of work needed to find a solution. Indeed, the problem may be undecidable, having no solution a computer can find, and have no decidable proof of its undecidability.

For easier problems, we have the distinction between P and NP. NP is the class of problems whose proof trace of steps to find the solution is polynomial in the length of the input. There are problems in NP that we are certain (though we cannot prove) require exponential time to find the solution in the first place. 

Note that this is a slightly different idea than the general computability distinction. The checker of a general program has to do the same work as the original program. However, it knows before it starts how long it will take. By contrast, most of the work done on a problem in NP by a solver is wasted. Therefore, while it spent exponential time, the actual trace generated is only polynomial length. It is precisely these problems that are in  NP. (We note that for a problem in NP, the best time cannot be worse that exponential. Indeed, a simple implementation searches for every possible proof, of which there are only an exponential number).

The general idea of these is that search is hard. It is always good to have others do the searching, and simply tell you how to go. 

This should be true for Notation3 rules as well. It turns out, that finding out how a decision was made is often more important that what the result was. Further, the party interested in computing a result may not be the party interested in its correctness. Generating proof allows for these jobs to be separated.  

Generating the proofs is reasonably straightforward. When a match is made, what was matched was stored. This combination of the rule, what was matched, and the result, is saved. When asked to print the proof, these are strung together.

One aspect of this strategy is that builtins must be handled separately. For most builtins, it suffices to have an object that simply knows which builtin was run. For builtins that run the reasoner recursively, like \qname{log:supports}, the proof can include a subproof. 

Towards that end, there is a proof format for Notation3. Continuing with the theme that there should be one format for both data and rules, the proof format is also in Notation3. In this way, tools to manipulate N3 can deal with proofs as well.

Nonetheless, the proof format runs into difficulties that other uses of Notation3 do not run into. Essentially, Notation3 turns out to be bad at talking about Notation3 --- we have still not reached a fully introspective language. These problems are mostly problems of denotation, including one that is also a problem of equality.

The problem of equality is mostly a problem of computational difficulty. Given two Notation3 formulae, are they equal? There are many different definitions of equality. Let us have an example. The following are four N3 formulae.
\begin{verbatim}
:A = {_:a :b :c . :c a :Q } .
:B = {:c a :Q . _:a :b :c } .
:C = {_:b :b :c . :c a :Q } .
:D = {_:a :b :c, _:e . :c a :Q } .
\end{verbatim}
Are $A,B,C,D$ equal? If we define equality as having the exact same serialization, then none of them are equal. If we say that reordering does not change identity, then $A$ and $B$ are equal. If we say that renaming variables does not change identity, then $A$ and $C$ are equal. Finally, if we say that if two formulae are true in the same interpretations, then $D$ is equal to the others. 

What is wrong with saying that they are all equal? The problem is that it is too limiting. We would like to be able to say
\begin{verbatim}
{@forAll :X . :X a [ owl:disjointWith :Immortal ] } # nothing is immortal
  :hasVariable :X .
\end{verbatim}
The question is: is \verb|:hasVariable| a valid predicate? It would be nice if it was. We would have a much easier time talking about N3 in N3, which is important in the proof format. We would like to say what a variable was bound to. In order to do that, we must be able to denote the variable from outside of its declaration. This is logically invalid. Therefore, we would like to at least allow this, and claim that there is some meaning to variable names in Notation3.

Given that, the problem of comparing two Notation3 formulae for equality is simple. Sort the two, and compare them. This is $O(n\log n)$ time, which is difficult to improve upon.

Of course, things are much worse. There is no requirement that a node even have a name. Thus, we note the following:
\begin{verbatim}
{ @forSome :x . :x a :Thing } :hasVariable :x .
{ [ a :Thing ] } :hasVariable :x .
\end{verbatim}
CWM will convert the first line into the second when processing a N3 file. Indeed, the ``\verb|[]|'' notation is used to allow for just that removal of unnecessary names. Even so, how can one refer to this node that was never named? Further, testing for equality just go much harder.

If we look at the proof ontology for Notation3 \footnote{The ontology appears at \uri{http://www.w3.org/2000/10/swap/proof}}, we note these problems show up. In order to say what variable bound to what, it explicitly says so. Variable names are represented as strings, in order to be able to refer to them unambiguously. Yet, when actually quoting the rule, the variables in the rule represent themselves.

The main purpose of a proof format is to show exactly what steps were taken. This way, a reader can follow those steps, verify their correctness, and thus verify the result.

Vagueness therefore does not support proofs. In general, a proof format should be able to say precisely what operations were done on precisely what data. Any less would be leaving too much to the reader.

Here we have a problem. In RDF, there anonymous nodes. These are very difficult to refer to unambiguously. Nodes that were never given names at all are particularly bad.

One option would be to have some standardized naming scheme based on location. Indeed, CWM does name anonymous nodes based on the line and column in the file. This is standardized nowhere, however. Further, this means that changing seemingly unimportant spacing in the RDF or Notation3 file would change the names of the nodes.
Further, many RDF tools will do other transformations including reordering the file.

\begin{table}[tb]
\label{table:cube}
\begin{verbatim}
_:a0 :p _:a1 . _:a1 :p _:a0 . 
_:a2 :p _:a3 . _:a3 :p _:a2 . 
_:a4 :p _:a5 . _:a5 :p _:a4 . 
_:a6 :p _:a7 . _:a7 :p _:a6 . 
_:a0 :p _:a2 . _:a2 :p _:a0 . 
_:a1 :p _:a3 . _:a3 :p _:a1 . 
_:a4 :p _:a6 . _:a6 :p _:a4 . 
_:a5 :p _:a7 . _:a7 :p _:a5 . 
_:a0 :p _:a4 . _:a4 :p _:a0 . 
_:a1 :p _:a5 . _:a5 :p _:a1 . 
_:a2 :p _:a6 . _:a6 :p _:a2 . 
_:a3 :p _:a7 . _:a7 :p _:a3 . 
\end{verbatim}
\caption{Some very symmetric Notation3}
\end{table}

 \begin{figure}[tb]
  \centerline{\epsfig{file=images/cube.pdf, height=4in}}
  \caption{A cube of anonymous nodes}
  \label{cube}
\end{figure}

As an example, let us look at the Notation3 in Table \ref{table:cube}. 
We can see the cube shape of this graph in Figure \ref{cube}. Note that all rotations of the nodes leaves everything the same. 
Because of the way Notation3 works, all blank nodes must be given names in the file. Nonetheless, there is no way to distinguish any of the nodes. They are all the same by rotations. If we were to compare this to another RDF file for equivalence, tools like \emph{cant}\cite{cant} will simply refuse.  

Cant \cite{cant} is an RDF canonicalizer. Given an RDF graph, it will try to find a canonical serialization for it, following techniques in \cite{Kelley:2003:GC}. If it can find canonicalizations for two files, then they are equivalent up to node renaming if and only if it gives the same canonicalizations. However, for harder cases like our cube it simply gives up. Further, it does not try to handle finding redundancy within an RDF graph. 

Finding redundancy is in general really hard. To decide if a graph is \emph{clean}, or has no redundancy, one needs to verify that there is no subset of the graph that entails the whole graph. To decide whether a particular subgraph entails the whole graph is at least as hard as graph-subgraph isomorphism, which is NP-Hard. This is worse, because a graph can be redundant in multiple ways. 

We can prove that RDF matching is at worst graph-subgraph isomorphism easily. If we want to find out if undirected graph $A$ is a subgraph of undirected graph $B$, in both replace each undirected edge with two edges, as in our cube. Then make an RDF graph $G$ that is $A \cup B$. Then we will see if this is equivalent to $B$. 

The good news is that people tend not to write RDF files that have structures like this. Indeed, almost all anonymous nodes that exist can be trivially proved to be ``nailed down'' by the properties that describe them in relation to named nodes. Thus, while this task is in the worst case still NP hard, in practice it is almost always much easier.

The other good news is that people tend to write clean RDF. Every once in a while a computer reasoner will make an RDF graph that is redundant, but these are usually pretty trivially redundant as well. Few operations actually create unclean RDF. 

The bad news is that there is a second type of node in Notation3 files that is difficult to uniquely identify. A quoted formula is identified only by its contents, which as we just demonstrated, is difficult to identify. 

Carlos Kloos has implemented an idea of hashing. By replacing every variable quantified at a level with the same value, we can recursively create a hash value for all kinds of Notation3 nodes such that two logically identical formulae have the same hash value, so long as they are both clean. Given that, different rules will have different hash values, and be identifiable easily. Because the proof process will not be creating spurious redundant triples, this is a sufficient definition of identity for the problem. This code was never integrated into the proof checker, so it is unknown how well it would work in practice. 
