使用列表规则在序言中进行前向链接

Question

在, we built a simple forward chaining in Prolog together with the user slago中解决了一些关于它的问题。前向链接代码：

:- op(1100, xfx, if).
:- op(1000, xfy, or).
:- op(900, xfy, and).                        

forward(Facts) :-
    fixed_point(nil, [true], Facts).                % Start with the base with only true

fixed_point(Base, Base, Base) :- !.                 % Reached a fixpoint
fixed_point(_, Base, Facts) :-                      % Base =/= Facts => not a fixpoint
    setof(Fact, derived(Fact, Base), NewFacts),     % Derive new facts
    ord_union(NewFacts, Base, NewBase),             % Add new facts to base
    fixed_point(Base, NewBase, Facts).              % Repeat with new base

derived(Fact, Base) :-                              
    rule(Fact if Condition),                        % Match a rule
    satisfy(Base, Condition).                       % Verify if condition is satisfied given base

satisfy(Base, G and Gs) :-                          % Condition is a conjunction
    !,
    member(G, Base),
    satisfy(Base, Gs).
satisfy(Base, G or Gs) :-                           % Condition is a disjunction
    !,
    (   member(G, Base)
    ;   satisfy(Base, Gs) ).
satisfy(_, callp(X)) :-                             % Condition is a callable fact
    !,
    call(X).
satisfy(Base, Condition) :-                         % Condition is an atomic proposition
    member(Condition, Base).

用于测试的简单知识库：

rule(eats_flies(fritz) if true).
rule(croaks(fritz)     if true).
rule(eats_flies(frotz) if true).
rule(croaks(frotz)     if true).
rule(sings(tweety)     if true).
rule(chips(tweety)     if true).
rule(has_wings(tweety) if true).
rule(croaks(krogr)    if true).
rule(chips(kroger)     if true).
rule(canary(X)         if and(sings(X),chips(X),has_wings(X))).
rule(frog(X)           if and(croaks(X),eats_flies(X))).
rule(green(X)          if frog(X)).
rule(yellow(X)         if canary(X)).
rule(node(a) if true).
rule(node(b) if true).
rule(node(c) if true).
rule(node(d) if true).
rule(node(e) if true).
rule(connected(a,b) if true).
rule(connected(b,c) if true).
rule(connected(c,d) if true).
rule(connected(d,e) if true).
rule(funny(c,d) if true).
rule(wonderful(X,Y) if or(nice(X,Y),funny(X,Y))).
rule(connected(X,Z) if and(connected(X,Y),connected(Y,Z))).
rule(path([Node|[]]) if node(Node)).
rule(path([Node, NextNode|Nodes]) if and(connected(Node, NextNode),path([NextNode|Nodes]))).
rule(int(1) if true).
rule(int(0) if true).
rule(int(2) if true).
rule(iszero(X) if and(int(X), callp(X = 0))).

rule(has_at_least_n([_|Tail], 0) if true).
rule(has_at_least_n([X|Tail], N) if and(node(X), callp(NewN is N-1), has_at_least_n(Tail, NewN))).
rule(has_at_least_n([X|Tail], N) if and(has_at_least_n(Tail, N))).

现在我想解决一个关于列表的最后规则的问题。我希望能够计算列表的元素。所以我希望能够说，例如，列表：

[a,b,c,d,e]

至少有 5 个节点，以及如下列表：

[a,x,y,c,d]

没有5个节点

使用我建立的规则，前向循环通过每次发现如下事实来循环自身：

has_at_least_n([_|_], 0)

因为每次它都可以将 _ 与任何东西统一起来。

关于我应该如何处理这种情况的任何提示？我如何制定避免无限循环的列表规则？

我的前锋仍然无法找到与 has_at_least_n([_|_], 0).

的虚拟规则不同的任何其他规则

编辑:

使用gtrace调试发现，如果and或or括号内有两个以上的事实，则不会被识别为satisfy(Base, G and Gs) / satisfy(Base, G or Gs)，但只有 satisfy(Base, Condition)，当然 member(Condition, Base) 是错误的，因为 and(..., ..., ..., ...) 不在 Base.

中

相反，当只有两个事实时，我在调试器中看到它们具有不同的表示形式：fact1 and fact2 这符合规则。

Answer 1

正如我之前所建议的，可能的解决方案如下：

:- op(1100, xfx, if).
:- op(1000, xfy, or).
:- op(900, xfy, and).

forward(Steps, FinalBase) :-
    forward_iteration(Steps, nil, [true], FinalBase).                 % Current base is [true]

forward_iteration(Steps, PreviousBase, CurrentBase, FinalBase) :-
    (   ( Steps = 0                                                   % Reached max iterations
        ; PreviousBase = CurrentBase )                                % Reached a fixed point
    ->  FinalBase = CurrentBase
    ;   setof(Fact, derived(Fact, CurrentBase), NewFacts),            % Derive new facts
        ord_union(NewFacts, CurrentBase, NewBase),                    % Add new facts into current base
        succ(Steps0, Steps),
        forward_iteration(Steps0, CurrentBase, NewBase, FinalBase) ). % Repeat with new base

derived(Fact, Base) :-
    rule(Fact if Condition),                                          % Match a rule
    satisfy(Base, Condition).                                         % Condition holds in current base

satisfy(Base, G and Gs) :-                                            % Condition is a conjunction
    !,
    member(G, Base),
    satisfy(Base, Gs).

satisfy(Base, G or Gs) :-                                            % Condition is a disjunction
    !,
    (   member(G, Base)
    ;   satisfy(Base, Gs) ).

satisfy(_Base, call(Fact)) :-                                        % Condition is a callable fact
    !,
    call(Fact).

satisfy(Base, Condition) :-                                          % Condition is an atomic proposition
    member(Condition, Base).

注意 and 是二元运算符，不是任意元数函子！因此，例如，我们可以将 len/2 定义为：

rule(item(X) if call(member(X, [a,b,c]))).
rule(len([], 0) if true).
rule(len([H|T], N) if len(T,M) and item(H) and call(succ(M,N))).

运行例子：

?- forward(1, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
FinalBase = [true, item(a), item(b), item(c), len([], 0)].

?- forward(2, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
len([a],1)
len([b],1)
len([c],1)
FinalBase = [true, item(a), item(b), item(c), len([], 0), len([a], 1), len([b], 1), len([...], 1)].

?- forward(3, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
len([a],1)
len([a,a],2)
len([a,b],2)
len([a,c],2)
len([b],1)
len([b,a],2)
len([b,b],2)
len([b,c],2)
len([c],1)
len([c,a],2)
len([c,b],2)
len([c,c],2)
FinalBase = [true, item(a), item(b), item(c), len([], 0), len([a], 1), len([a|...], 2), len([...|...], 2), len(..., ...)|...].

使用列表规则在序言中进行前向链接

Forward chaining in prolog with rules about lists

prolog

swi-prolog

编辑: