0

这是我的代码，用于 Satchmo 定理证明。它做了一些统一。

:- op(700, xfx, ==>).
:- op(400, yfx, &).
:- op(400, yfx, or).

fact([a, 9]).
fact([b, 9]).
rule([a, X] & [b, X] ==> [c, X]). %% horn bit
rule([c, X] ==> [r, X] or [s, X]). %% non horn bit
rule([r, X] ==> [t, X]).
rule([s, X] ==> [t, X]).

horn(A & B) :- 
    !,
    horn(A),
    horn(B).
horn(A or B) :-  
    !,
    (horn(A); horn(B)).
horn(P) :-
    fact(P).
horn(P) :-
    temp(P). 
horn(P) :-
    rule(SUBGOALS ==> P),
    \+ P = (_A or _B),
    horn(SUBGOALS).

satchmo(P) :-
    retractall(temp(_)),
    prove(P).

prove(P) :-
    horn(P).
prove(P) :-
    rule(LHS ==> (A or B)),
    horn(LHS),
    \+ horn(A or B),

cprove(A ==> P), 
    cprove(B ==> P). 

cprove(A ==> P) :-
    try(A),
    (prove(P) ->
    untry(A);
    (untry(A), fail)).

try(A & B) :-
    !,
    try(A),
    try(B).
try(A) :-
    assert(temp(A)).

untry(A & B) :-
    !,
    untry(A),
    untry(B).
untry(A) :-
    retract(temp(A)).

要了解它是如何工作的，我们可以通过 ?- spy([satchmo]) 来做到这一点。

1-如果给定的查询是事实：

?- satchmo([a, 9]). 
yes.

或者

?- satchmo([b, 9]).
yes.

该程序将证明它是事实。

2-如果喇叭位中的查询为：

?- satchmo([c, 9]). 
yes.

该程序将证明它，因为它是喇叭规则。

3-如果非喇叭位中的查询为：

?- satchmo([t, 9]). 
yes.

也会被证明的。

这是完美的工作。但是当我试图改变它时。我需要做另一种可以证明以下内容的匹配，而不是统一：

如果我有：

rule[living, X] ==> [mortal, X]. 
[man, socrates].

我想证明：

?- satchmo([mortal, socrates]). 
yes.

为此，我稍微修改了我的代码，而不是：

horn(P):-
    fact(P).

我放了一些非常相似的东西：

horn(P):-
    match(P, P0),
    fact(P0).

我将匹配定义为：

match(X, Y):-
    X=Y.

我知道我没有通过这一举动做任何事情，但我正在考虑修改 match 的定义以能够证明我需要什么。

我被困在这里的某个地方，看看我当前的代码。

:- op(700, xfx, ==>).
:- op(400, yfx, &).
:- op(400, yfx, or).
:- op(400, yfx, <<<).

fact([a, 9]).
fact([b, 9]).
rule([a, X] & [b, X] ==> [c, X]). %% horn bit
rule([c, X] ==> [r, X] or [s, X]). %% non horn bit
rule([r, X] ==> [t, X]).
rule([s, X] ==> [t, X]).

man <<< human.
human <<< animal.
animal <<< living.

subset(X, X).
subset(X, Y) :-
    X <<< Y.
subset(X, Z) :-
    X <<< Y,
    subset(Y, Z).

horn(A & B) :- 
    !,
    horn(A),
    horn(B).
horn(A or B) :-  
    !,
    (horn(A); horn(B)).
horn(P) :-
    fact(P).
horn(P) :-
    temp(P). 
horn(P) :-
    rule(SUBGOALS ==> P),
    \+ P = (_A or _B),
    horn(SUBGOALS).

satchmo(P) :-
    retractall(temp(_)),
    prove(P).

prove(P) :-
    horn(P).
prove(P) :-
    rule(LHS ==> (A or B)),
    horn(LHS),
    \+ horn(A or B),
    cprove(A ==> P), 
    cprove(B ==> P). 

cprove(A ==> P) :-
    try(A),
    (prove(P) ->
    untry(A);
    (untry(A), fail)).

try(A & B) :-
    !,
    try(A),
    try(B).
try(A) :-
    assert(temp(A)).

untry(A & B) :-
    !,
    untry(A),
    untry(B).
untry(A) :-
    retract(temp(A)).

在这里，我们可以测试子集：

?- subset(human, man). 
yes.

这里的问题是我不知道如何通过证明来实现我的目标：

?- satchmo([mortal, socrates]).
yes.

从：

[living, X] ==> [mortal, X]. 
[man, socrates].

可以通过更改匹配的定义来完成吗？如果没有，有没有其他方法可以做到这一点？

4

1 回答 1

0

OK完成，

这个问题的解决方法很简单，就是改变match的定义，所以会如下：

match(P, P0) :-
    P = [X, _],
    P0 = [Y, _],
    subset(Y, X).

subset(X, X).

subset(X, Y) :-
    X <<< Y.

subset(X, Z) :-
    X <<< Y,
    subset(Y, Z).

当我有这个事实时：

fact([man, socrates]).
man <<< human.
human <<< animal.
animal <<< living.

这个规则：

rule([living, X] ==> [mortal, X]).

我可以证明：

?- satchmo([mortal, socrates]).
于 2014-02-03T07:50:25.967 回答