Search code examples
prolog

Implementation of forward chaining in prolog (SWI-Prolog)

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. gtrace status

Solution

  • 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).