\chapter{Conclusion and Lessons Learned}
\comment{
RDF and proofs don't mix well.
Order is important if order is to be maintained.
Making systems that operate monotonically in an open world is possible, and has very nice properties for distribution (important for the web). That said, saying things gets hard enough that controlling the computations done is nontrivial.
Just having the data out there is often the best you can do --- translating it into usable form is usually the easiest step.
The problem is one of consistently naming things.


There are three main conclusions, in regard to three things. 
There are also minor conclusions.
}

Over the course of this work, a number of conclusions were reached. Many more things were inconclusive, or point to further work that needs to be done. Mixing rules from different sources was found to have implications on both the language and the reasoners used. There is further work to be done with reasoning strategies and proofs. The styles of rules encountered have other lessons. 

A big effort by Cwm is to treat rules as data. This allows for one to talk about rules, and possibly reason over them. Naming rules, as in AIR, seems to make this easier in some senses, by making it clearer the identity of the rule. On the other hand, making a rule take up more that one RDF statement has a cost in simplicity of implementation. When treating rules as data, it become possible for a rule to suddenly appear.

In regard to choices of reasoning strategy, there are no global maxima. There exist rules for which nothing will run well, and trivial things everything will run well. In between, there is a range of problems, datasets, and rule sets. Different rule sets will be optimized for different rule techniques. In particular, some will work better with a forward chainer, others a backward chainer. It may bear investigation whether a reasoner that can make good guesses about which technique to use could be written. However, any attempts at this may well run into the halting theorem.

Rule sets vary a great deal. If one is not careful, one can write one that can loop forever. By the halting theorem, there exists a rule set that cannot be proved whether or not it loops forever on particular data. One can write a rules set that is highly inefficient on any reasoner\footnote{see Appendix \ref{evil-n3}}. Given the different behaviors of various algorithms, there are many rule sets that are optimized for a particular style of reasoning. Despite the general meaning of a rule, in practice authors write rules for a particular engine. 

Rules therefore must be handled with care. Any rule engine looking at the web for rules to run will run into rules that are highly inefficient on it. Putting resource limits on the reasoner in these cases would be appropriate. Looking into this would be interesting. 

Another thing to look into would be further distribution and multithreading of rule reasoning. Given that Notation3 rules are monotonic, any split of the reasoning task is unlikely to be harmful. 

Debugging when rules fail to get a result is a pain, and any rule based system should have something to help do this. 

In regard to AIR, more work is needed for its main features. Not enough is understood about the behavior of AIR rules when processed. For instance, for complete correctness, a goal should match a goal rule if they unify at all. In the reasoner, for there to be acceptable performance, there needs to be full entailment. 

This difficult to understand behavior is especially bad for the person writing the rules. Exactly how a rule is written can have very large effects on the efficiency of its processing. If techniques like AIR are to become useful, programmer effort must be decreased. 

In regard to the explicit goal tracking, things are mixed. There are gains there, but they are not for all cases. This is a problem of scalability --- it can help if the facts vastly outnumber the rules. Some of the gain from these rules comes from careful ordering of the match. If one does a dynamic ordering, then this is done more intelligently with much less work on the part of the programmer. 

The AIR \qname{air:alt} feature, to allow for closed-world reasoning, needs more work. Without a clear semantics, the writer of the reasoning engine and the reader of the justification trace are both likely to be confused. Unlike \qname{log:notIncludes}, this solution is not straightforward. That said, it accomplishes its goal of making certain classes of statements much easier to make.

In regard to a proof language for RDF rules, more work needs to be done. Even naming rules like AIR does should help. Hashing to identify formulae would also help. Having a way of uniquely referring to triples or anonymous nodes within the proof language would be even better. This proof language would then not be RDF based, but something else. 

The essential problem was with ordering. Matching unordered things in the presence of anonymous nodes is hard. While this is rarely an issue in regular RDF, in proofs these can show up a lot. Notation3 has no good way to name anonymous nodes, for obvious reasons. 

Proofs generated by computers are, in general, caught in many little details. Readability is at best hard. The work on AIR justifications generates things that would be even harder to check. Nonetheless, this work has succeeded at improving readability.

More work is needed for an easily checked proof language. Such a language would represent RDF in an unambiguous fashion, to be able to represent each proof step precisely. Given that, checking a proof takes linear time in the length of the proof. This development would be important for the usefulness of proofs on the Web. Given that information on the Web is often not trustworthy, knowing why a conclusion is reached is often as important as the conclusion, having a good system for storing and transmitting these is useful. 

In summary, rules can be an effective tool on the Semantic Web. Perhaps with a better proof system, it would be possible to refer to rules and data and the conclusions based on them in a general way. In many ways, rules are too powerful to not be used, but even our current best, still often difficult to use. 

