Rule based forward reasoner

One main contribution of this project is a rule based forward reasoner. It is not the only rule based reasoner there is, but this is mine. On this page I will explain the main concepts behind this and try to give you a better understanding on how things work, and why they are done that way.

[[TOC]]

The name / what it is

It is called a "rule based forward reasoner" for a reason. First of all it is rule based since everything that is inferred is done so though rules, implications, if - then - constructs, if you like. The pattern is always the same: Given a set of preconditions and effects, the effects are executed when a match for the preconditions is found. It works forwards, as it always checks for the conditions first and executes the effects afterwards. There is no backward reasoning, where you ask the reasoner if a fact holds and the reasoner starts checking given the rules and data. This has a very important implication: Everything that can be inferred through the given rules, will be inferred whenever possible. The reasoner always holds the complete knowlege explicitely. Take this into account if some of your rules require computationally expensive operations, or the amount of data that can be inferred is huge.

Last but not least it is a reasoner, not only a production rule system. Inferred knowledge is added to the knowledge base and the rete network and is taken into account for further rule activations. Furthermore it tracks the origin of information, can explain where things came from, and most importantly, deal with non monotonic updates: You can retract or update data, and the reasoner will react with incremental updates. It retracts only the inferences it needs to, and on assserting facts only processes newly found matches. The reasoner does not need to start from scratch when you retract some information.

Negations / inconsistencies / open world

Since the reasoner relies on the rete pattern matching algorithm to find matches for the preconditions of the rules, it does not explicitely model negations. There is no if not <fact> then -. Therefore it does not detect inconsistencies in your data, either, but stupidly executes your rules. This also implies that there can be no negation in a rules effect: if - then not <fact> can not be expressed in this system. What you can do is include the negation in your data instead, i.e. if - then <not fact> would work, though you will have to take care of inconsistencies yourself. The reasoner will happily infer <fact> and <not fact> for you, if the rules allow it to.

There is only one form of "negation" you can use in the rules: Following the concept of an open world assumption, the keyword noValue allows you to check in a precondition if a given information has not yet been inferred or asserted. It is not the explicit "not" you might want, but is a helpful tool in many situations.

Evidence / non monotonic / inference loops

When working in a completely monotonic domain, i.e. you only ever add facts to your knowledge base and never remove them, managing the inferred knowledge is easy as you only have to keep a list of the inferred statements. But in general things are not monotonic: A robots environment changes, things appear and disappear, and maybe you even have some rules that infer things when there is no match for some pattern (remember noValue?). As soon as you add a fact that leads to a positive match of that pattern you will need to retract the previously inferred information. But wait -- are you really sure? Or are there other rules that infer the same information on different paths, so that it might still be valid?

To handle this problem, the reasoner needs to keep track of why data is kept in its knowledge base, in order to remove it as soon as there is no such reason anymore. The term I chose for these reasons is Evidence. (Yes, I know this might be misleading, and maybe it should be changed, but for now it works...).

There are two types of evidence: AssertedEvidence describes that some knowledge is externally asserted and can be assumed to hold. It is used to assert the basic information that you give to the reasoner to work with. You can use the same evidence instance to assert multiple facts, which allows you to remove all those facts together by removing the evidence (but you can still remove a single fact-evidence pair if you do not want the remove everything). AssertedEvidence are identified by a unique name.

The other type is the InferredEvidence. It consists of a token representing the match for the preconditions of a rule and the production that created the new working memory element as an effect. When the same production gets activated with a RETRACT for the same token, the reasoner removes the evidence, and all WMEs which do not have any evidences left. To avoid dangling inference-circles, the reasoner performs some additional checks and enforces that every inferred WME is in the end based on knowledge supported by AssertedEvidence.

There is a very simple example for these inference loops: Take a look at the equivalent property. If a is equivalent to b, well, then b is equivalent to a, too, right?

(?a <equivalent> ?b) -> (?b <equivalent> ?a)

When we add the fact (<A> <equivalent> <B>) we get the following evidences:

(<A> <equivalent> <B>) is asserted
(<B> <equivalent> <A>) is inferred from (<A> <equivalent> <B>)
(<A> <equivalent> <B>) is inferred from (<B> <equivalent> <A>)

If we simply remove the previously asserted statement, we remain with a dangling inference loop:

(<B> <equivalent> <A>) is inferred from (<A> <equivalent> <B>)
(<A> <equivalent> <B>) is inferred from (<B> <equivalent> <A>)

Of course, things can become way more complex. Hence, whenever an evidence is removed, be it from the outside or internally through inferencing, a check is performed starting from the fact for which the evidence is removed. The goal is not to traverse the whole graph and find all cycles, but to confirm that the one affected fact is still grounded in assertions. To do so, the following algorithm is implemented:

Assume that the fact does not hold, and check if any of its evidences is still valid under this assumption. If any of them is we are good and do not need to remove the fact. If none is, all evidences for the fact rely in some way on the fact itself, so we have a cycle to tear down.

An evidence is valid if it is an AssertedEvidence, or an InferredEvidence for which all WMEs/facts involved still hold. To check the facts in the inferred evidence, the algorithm recurses, adding the facts to this list of facts we assume to not hold, in order to break any cycle. If a fact is found to be valid it is removed from the list. At the end we know if the fact we wanted to check is still valid, and if not we also have a list of facts that do not hold anymore and are part of the cycle that held the original fact alive. All of them are removed from the reasoner and the rete network, and thus evidences containing these facts are removed, too, as part of the usual inference process.

Yes, this is quite a bit overhead. But necessary when dealing with non-monotonic reasoning. After all, there is no free lunch.

Explanations

One neat side effect of keeping track of all evidences for our knowledge is the possibility to explain it. The reasoner grants access to its current inference state, which in turn can be iterated to create a graphical representation of the inference path for a given WME. Please refer to the Examples page for more information.

The RuleParser

The RuleParser allows you to write rules as strings and parses them to create a corresponding rete network. To be able to do so it uses node builders and accessors:

NodeBuilders implement the logic to create the nodes for a specific condition, builtin or effect based on a string identifier and a list of arguments. The Accessors are used to abstract from the WME types and provide access to basic internal types, like numbers and strings.

While constructing the nodes for a rule, the parser keeps track of the current variable bindings: A binding is a mapping from a variable name (e.g. ?foo) to an accessor, which describes how to get the value from a token at this point in the rule/in the nework. The node builders that are used to create the nodes for the conditions know the return values of the nodes or the internals of the WME types they check, and bind specific accessor objects to the variables. They also check if e.g. the given arguments are of correct type and throw exceptions if not -- incorrect rules already throw while trying to parse them.