Prolog 中前向链接的实现 (SWI-Prolog)

Question

我想在 Prolog 中实现前向链接推理。我编写了一个简单的事实知识库和一些规则，从中我应该能够得到事实green(fritz)。我尝试实现它，但不知怎的，当member失败时，它就停止了。

/*
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).

重点关注forward_rule实施，我想检查是否fact在tail规则中。如果是，则应将其删除。如果没有，我应该继续fact从所有规则中删除它。然后，通过forward_chaining实施，应该为每个fact. 当然，如果tail为空，则head应该成为一个新的fact。如果tail不为空，则rule必须更新。

我错过了什么吗？

编辑1：

在伊莎贝尔新手回答后，我尝试修复代码。现在 if-then-else 可以正常工作了。但是，递归调用forward_rule在开始之前仍然失败。

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

我用来gtrace尝试理解代码在哪里失败。所以我看到它没有进入递归调用。似乎存在统一问题，但我不明白为什么。

Answer 1

为了正确工作，前向链接算法不能删除或修改每次迭代中触发的规则（否则该实现将不适用于递归规则）。当获得固定点时（或者，当导出要证明的基本事实时） ，算法终止。

为了更统一的表示，事实可以表示为带有条件的规则true。此外，为了区分不同的知识库，可以用知识库标识符来标记规则。

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

例子：

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

备注只要知识库是无函数的（即，它具有有限 Herbrand 模型），就存在最小固定点。