Implementation of forward chaining in prolog (SWI-Prolog)

Question

I would like to implement forward-chaining reasoning in Prolog. I made up a simple KB of facts and some rules, from which I should be able to get the fact green(fritz). I tried to implement it but somehow, when member fails, it stops going on.

/*
meta rules
*/

rule(1, [canary(X)], [sings(X), chips(X)]).
rule(2, [frog(X)], [croaks(X), eats_flies(X)]).
rule(3, [green(X)], [frog(X)]).
rule(4, [yellow(X)], [canary(X)]).

/*
meta facts
*/

fact(1, eats_flies(fritz)).
fact(2, croaks(fritz)).
fact(3, sings(tweety)).
fact(4, chips(tweety)).
fact(5, croaks(kroger)).
fact(6, chips(kroger)).

/*
forward chaining
*/

start_id(100000).

get_id(Y) :-
    retract(start_id(X)),
    Y is X + 1,
    assert(start_id(Y)).

forward(NewFacts) :-
    findall(rule(Id, Head, Tail), rule(Id, Head, Tail), Rules),
    findall(fact(Id, X), fact(Id, X), Facts),
    forward_chaining(Rules, Facts, NewFacts).

forward_chaining(_, [], _).
forward_chaining([], _, _).
forward_chaining([rule(Id, Head, Tail)|Rules], [fact(Id, X)|Facts], NewFactsRec + NewFactsRecRec) :-
    forward_rule([rule(Id, Head, Tail)|Rules], fact(Id, X), NewFactsRec, NewRulesRec),
    forward_chaining(NewRulesRec + Rules, NewFactsRec + Facts, NewFactsRecRec).

forward_rule([], _, _, _).
forward_rule([rule(Id, Head, Tail)|Rules], fact(Id, X), NewFacts, NewRules) :-
    member(X, Tail) ->
        (    
            delete(Tail, X, NewTail),    
            NewTail = [] ->
                get_id(NewId),
                NovelFact = [fact(NewId, Head)],
                NovelRule = []
                ;
                NovelFact = [],
                NovelRule = [rule(Id, Head, NewTail)]
            
        );
        NovelRule = [rule(Id, Head, Tail)],
    forward_rule(Rules, fact(Id, X), NewFactsRec, NewRulesRec),
    append(NewRulesRec, NovelRule, NewRules),
    append(NewFactsRec, NovelFact, NewFacts).

Focusing on the forward_rule implementation, I would like to check if the fact is in the tail of a rule. If it is, then it should be removed. If not, I should go on removing the fact from all the rules. And then, via the forward_chaining implementation, that should be done for every fact. Of course, if the tail is empty, the head should become a new fact. If the tail is not empty, the rule must be updated.

Am I missing something??

EDIT 1:

After Isabelle Newbie's answer I tryied to fix the code. Now the if-then-else are working properly. But still, the recursive call to forward_rule fails before starting.

start_id(100000).

get_id(Y) :-
    retract(start_id(X)),
    Y is X + 1,
    assert(start_id(Y)).

forward(NewFacts) :-
    findall(rule(Id, Head, Tail), rule(Id, Head, Tail), Rules),
    findall(fact(Id, X), fact(Id, X), Facts),
    forward_chaining(Rules, Facts, NewFacts).

forward_chaining(_, [], _).
forward_chaining([], _, _).
forward_chaining([rule(Id, Head, Tail)|Rules], [fact(Id, X)|Facts], NewFacts) :-
    forward_rule([rule(Id, Head, Tail)|Rules], fact(Id, X), NewFactsRec, NewRulesRec),
    writeln('going on'),    % debug
    append(Rules, NewRulesRec, ToForwardRules),
    append(Facts, NewFactsRec, ToForwardFacts),
    forward_chaining(ToForwardRules, ToForwardFacts, NewFacts).



forward_rule([], _Fact, [], []).
forward_rule([rule(Id, Head, Tail)|Rules], fact(Id, X), NewFacts, NewRules) :-
    (   member(X, Tail) 
    ->  delete(Tail, X, NewTail),
        writeln('is member'),    % debug
            (   NewTail = [] 
            ->  get_id(NewId),
                writeln('newtail is empty'),    % debug
                NovelFact = [fact(NewId, Head)],
                NovelRule = []
            ;
                writeln('newtail is not empty'),    % debug
                NovelFact = [],
                NovelRule = [rule(Id, Head, NewTail)])
            
    ;
        writeln('is not member'),   % debug
        NovelRule = [rule(Id, Head, Tail)],
        NovelFact = []),
    writeln('postlude'),    % debug
    forward_rule(Rules, fact(Id, X), NewFactsRec, NewRulesRec),
    append(NewRulesRec, NovelRule, NewRules),
    append(NewFactsRec, NovelFact, NewFacts).

I'm using gtrace to try to understand where the code fails. So I saw that it is not entering the recursive call. It seems that there is an unification problem, but I don't understand why.

Answer 1

To work correctly, the forward chaining algorithm cannot remove, nor modify, the rules that are fired in each iteration (otherwise the implementation will not work for recursive rules). The algorithm terminates when a fixpoint is obtained (or, alternatively, when a ground fact to be proved is derived).

For a more uniform representation, facts can be represented as rules with condition true. Also, to distinguish different knowledge bases, rules can be labeled with a knowledge base identifier.

:- op(1100, xfx, if).
:- op(1000, xfy, and). % <== EDITED

forward(KB, Fact) :-
    fixpoint(KB, nil, [true], Facts),
    member(Fact, Facts).

fixpoint(_, Base, Base, Base) :- !.
fixpoint(KB, _, Base, Facts) :-
    setof(Fact, derived(Fact, KB, Base), NewFacts),
    ord_union(NewFacts, Base, NewBase),
    fixpoint(KB, Base, NewBase, Facts).

derived(Fact, KB, Base) :-
    rule(KB : Fact if Condition),
    satisfy(Base, Condition).

satisfy(Base, Condition) :-
    (   Condition = (A and B)
    ->  member(A, Base),
        satisfy(Base, B)
    ;   member(Condition, Base) ).


% first knowledge base

rule(1 : eats_flies(fritz) if true).
rule(1 : croaks(fritz)     if true).
rule(1 : sings(tweety)     if true).
rule(1 : chips(tweety)     if true).
rule(1 : has_wings(tweety) if true). % <== EDITED
rule(1 : croaks(kroger)    if true).
rule(1 : chips(kroger)     if true).
rule(1 : frog(X)           if croaks(X) and eats_flies(X)).
rule(1 : green(X)          if frog(X)).
rule(1 : yellow(X)         if canary(X)).
rule(1 : canary(X)         if sings(X) and chips(X) and has_wings(X)). % <== EDITED

% second knowledge base (recursive example)

rule(2 : connected(a,b) if true).
rule(2 : connected(b,c) if true).
rule(2 : connected(c,d) if true).
rule(2 : connected(X,Z) if connected(X,Y) and connected(Y,Z)).

Examples:

?- forward(1, canary(X)).
X = tweety ;
false.

?- forward(1, green(X)).
X = fritz ;
false.

?- forward(2, connected(a,X)).
X = b ;
X = c ;
X = d ;
false.

Remark A least fixpoint exists whenever the knowledge base is function-free (i.e., it has a finite Herbrand model).

Answer 2

There are several problems here.

Problem 1 is that the non-recursive clauses for your recursive predicates look like this:

forward_rule([], _, _, _).

This means: "If the list of rules is empty, arbitrary facts correspond to arbitrary new facts and arbitrary new rules."

For example:

?- forward_rule([], apple_pie, [new_fact_1, new_fact_2, new_fact3], [new_rule_1, new_rule_2]).
true.

You almost certainly meant something more like:

forward_rule([], _Fact, [], []).

meaning: "If the list of rules is empty, no matter what _Fact might be, there are no new facts and no new rules to derive."

Problem 2 is in lines like this:

forward_chaining(NewRulesRec + Rules, NewFactsRec + Facts, NewFactsRecRec).

This looks a bit like you're trying to use + as a list append function. There are no functions in Prolog. You know how to use append, but you will have to use it for this as well.

Problem 3 is around your if-then-else code. Your formatting doesn't reflect what will actually happen.

Consider:

conditional(C) :-
    writeln(unconditional_prelude),
    C = true ->
        (
            writeln(true_branch_1),
            writeln(true_branch_2)
        );
        writeln(presumably_false_branch),
    writeln(presumably_unconditional_postlude).

This gives:

?- conditional(true).
unconditional_prelude
true_branch_1
true_branch_2
true.

?- conditional(false).
unconditional_prelude
presumably_false_branch
presumably_unconditional_postlude
true.

See how non-indented part "after" the conditional is in fact part of the false branch?

Often a separate predicate definition can be clearer than the if-then-else construct. For example, you could write something like:

x_tail_novelfact_novelrule(X, Tail, NovelFact, NovelRule) :-
    member(X, Tail),
    ... rest of "true" branch ...
x_tail_novelfact_novelrule(X, Tail, NovelFact, NovelRule) :-
    \+ member(X, Tail),
    ... rest of "false" branch ...

If you must use the if-then-else construct, you must put parentheses around the whole if-then-else. Like this:

... prelude ...
(    Condition1,
     Condition2
->   TrueBranch1,
     TrueBranch2
;    FalseBranch1,
     FalseBranch2 ),
... postlude ...

Only (at most) one of the branches will be executed. No matter which branch is executed, if it succeeds, then the postlude will be executed.

There might be other problems with your code as well, but I hope this helps get you started with fixing things for now.