.. _section-How Flora Answers Queries:

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 :ref:`section-Queries and Latent Queries`, we saw examples of queries with a single goal, such as:

.. code-block:: flora

    Greg [ child -> ?x ].

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

.. code-block:: flora

    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,

.. code-block:: flora

    Greg [ child -> ?x ]

unifies with

.. code-block:: flora

    Greg [ child -> Louisa ]

by variable substitution ?x = Louisa.

For a slightly more complex case, the following:

.. code-block:: flora

    Emma [ child -> ?x ]

unifies with

.. code-block:: flora

    ?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.