How Flora Answers Queries

As in Prolog, the reasoning algorithm essentially consists of unification and backtracking. We give only a brief, informal description here. Refer to a basic text on Prolog for a deeper treatment of this topic.

Ideally, we think of our Flora rules and ontologies as logical axioms, with a declarative meaning. In this view, executing a query means asking the reasoner to find a logical proof. But sometimes it is necessary to understand how the reasoner goes about doing this. This is called the operational semantics of the system.

When we issue a query, we give the reasoner one or more goals. In Section Queries and Latent Queries, we saw examples of queries with a single goal, such as:

Greg [ child -> ?x ].

and in Section ’and’ and ’or’, we introduced queries with multiple goals, which are combined using the \and or the comma operator, for example:

Louisa [ parent -> ?p ] \and ?p [ parent -> ?Grandparent ].

When given multiple goals, Flora will work on them in the order they are given, from left to right.

To prove a goal, Flora looks for facts that unify with the goal, or rules whose head unify with the goal. Two Flora terms A and B unify if and only if there is a variable substitution that makes the terms equal. For example,

Greg [ child -> ?x ]

unifies with

Greg [ child -> Louisa ]

by variable substitution ?x = Louisa.

For a slightly more complex case, the following:

Emma [ child -> ?x ]

unifies with

?y [ child -> Isobel ]

by variable substitution ?x = Isobel, ?y = Emma.

If Flora finds a fact that unifies with the goal, the variables in all the goals following (if any) are instantiated according to this variable substitution, and Flora goes on to prove the next goal. When all the goals have been proved, the final variable substitution constitutes a solution. Flora will then backtrack (go backwards) through the list of goals, to try to find more solutions. First, it tries to find more solutions for the last goal. If that fails, it continues to the goal before that, and so on. Any variable substitutions that were performed when the previous solution was found are undone to the point of backtracking.

If Flora finds a rule whose head unifies with the goal, the variable substitution is applied to the rule body, and all the terms in the rule body become new goals. Backtracking to find more solutions works just as discussed above. Variable substitutions that are performed as a result of executing goals in a rule body are also applied to the rule head! Indeed, this is how information is passed out of rules.

Note that each rule has its own variable scope, so there is no connection between variables of the same name in two different rules.

This approach to reasoning is often called backwards chaining (because we use the rules “backwards” from consequents to antecedents), or goal-directed. This is in contrast to forward chaining systems, which essentially work in the opposite way (this approach is common in so-called production rules systems). We can also note that the reasoning is depth-first. That is, Flora must completely evaluate a goal, and all it’s sub-goals contained within, before it can move on to the next goal.

One helpful way to understand how Flora reasoning works is to use the explanation facility in the Sunflower Query Results tab on different query results such as those produced by executing queries in family.flr. The explanations show instantiated rules and facts used to derive a solution. Note that these explanations only show successful paths of goal execution, with all variable substitutions performed.

In the next section, we give a step-by-step example, that also explains the order of steps performed, intermediate variable substitutions, and backtracking.