Example of Goal Execution

Here we give a short example of Flora goal execution. The query we want to execute is Louisa [ancestor -> ?Ancestor], i.e., we want to find all of Louisa’s ancestors, and the knowledge base is as follows (this is a portion of the family.flr ontology that comes with the Sunflower distribution):

@!{ParentRule}
?Person [parent -> ?Parent] :-
  ?Parent [child -> ?Person].
@!{AncestorRule_Base}
?Person [ancestor -> ?Ancestor] :-
  ?Person [parent -> ?Ancestor].
@!{AncestorRule_Rec}
?Person [ancestor -> ?Ancestor ] :-
  ?Person [parent -> ?Parent],
  ?Parent [ancestor -> ?Ancestor].
Greg : Man [
  child -> {Kellie, Louisa},
  spouse -> Grit,
  birthDate -> "1991-04-27"^^\date].
Dana : Woman [
  child -> {Greg, Herb},
  birthDate -> "1967-06-09"^^\date].

First, as mentioned in Section Facts, we must remember that the composite facts about Greg and Dana are shorthand for a number of simple facts: Greg : Man, Greg [ child -> Louisa ], and so on. Flora uses these simple facts during reasoning.

Now, when it gets the goal Louisa [ancestor -> ?Ancestor], Flora has two choices. Either use AncestorRule_Base or AncestorRule_Rec. There are no facts that unify with the goal, and we are disregarding tabling for now (see The Effect of Tabling). The choice between the two rules is non-deterministic [1]. Suppose Flora picks AncestorRule_Base. Then ?Person is unified with Louisa, and ?Ancestor in the rule head with ?Ancestor in the goal. Note that these two variables are only “accidentally” named the same [2]. This leaves us with a new goal from the rule body, with the variable substitution applied, i.e. Louisa [parent -> ?Ancestor]. There is only one choice for resolving this goal, ParentRule. Unifying Louisa [parent -> ?Ancestor] with the rule head, we get the variable substitution ?Person = Louisa (again) and ?Parent = ?Ancestor. Our new goal from the rule body is now ?Ancestor [ child -> Louisa ]. This unifies with one fact, Greg [ child -> Louisa ], with the variable substitution ?Ancestor = Greg. There is no remaining goal, so this variable substitution constitutes a solution to the original query!

Next, the reasoner will backtrack through the previous goals, looking for different ways of resolving them. The first “choice point” (going backwards) is where we chose to use AncestorRule_Base to prove the goal Louisa [ancestor -> ?Ancestor] (i.e., we have to backtrack all the way to the very beginning of our computation). Now we choose AncestorRule_Rec instead. As before, we get the variable substitution ?Person = Louisa, ?Ancestor = ?Ancestor. Our new goals from the rule body are: Louisa [parent -> ?Parent] and ?Parent [ancestor -> ?Ancestor]. For the first goal, we use ParentRule and get ?Parent = Greg, similarly to what happened in our first solution. We apply this variable substitution to our second goal, yielding Greg [ ancestor -> ?Ancestor ] as our new goal. Again, we have a choice of the two AncestorRules. Flora might pick AncestorRule_Base. This produces the new goal Greg [ parent -> ?Ancestor ]. To resolve this goal, ParentRule is used, and we get the new goal ?Ancestor [ child -> Greg ]. This unifies with the fact Dana [ child -> Greg ], with the substitution ?Ancestor = Dana, and this is our second solution.

Flora will again backtrack, and try to find additional ancestors of Dana’s, but this fails because we don’t have any information about Dana’s parents.

As mentioned above, it may be helpful to execute and trace these goals in Sunflower to get a better idea of what the final proofs look like.

[1]	Unlike in Prolog, where the first rule is always picked first

[2]	In reality, the reasoning engine has to rename variables in some cases to avoid incorrect unifications