Recursion and the fixed point

world open.
jacob[father -> isaac; mother -> rebekah].
isaac[father -> abraham; mother -> sarah].
sarah:Woman.
rebekah:Woman.
?Child[parent -> ?Parent] <- (
    ?Child[father -> ?Parent] OR ?Child[mother -> ?Parent]
).
?Child[ancestor -> ?Parent] <- ?Child[parent -> ?Parent].
?Child[ancestor -> ?Ancestor] <-
    ?Child[parent -> ?Parent]
    AND ?Parent[ancestor -> ?Ancestor].
?- jacob[ancestor -> ?Ancestor] AND ?Ancestor:Woman.
expect true: jacob[ancestor -> sarah].

First derive parent edges. Then derive direct ancestors and repeatedly extend them through parents. The query returns Rebekah and Sarah. Sarah requires a path through Isaac.

FrameX evaluates finite rule consequences in synchronous rounds until no new facts are added. Source order is not an execution schedule. A recursive rule does not mean “call this procedure again” or perform Prolog-style backtracking.

Every variable in the head must be positively bound in each applicable branch of the body. This keeps the rule grounded in supplied knowledge. No new people are generated by recursion.

Explain an answer

Use framex explain with this file and the quoted query 'jacob[ancestor -> sarah]'. Identify the source facts and intermediate parent/ancestor conclusions. More than one proof can support the same logical fact.

Try it

Draw the graph and mark which relationships are input facts and which are derived. Predict the effect of removing Isaac’s mother edge.