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.

この動きによって何もしていないことはわかっていますが、必要なことを証明できるように、一致の定義を少し修正することを考えています。

ここのどこかで立ち往生しています。現在のコードを見てください。

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

わかりました、完了しました、

この問題の解決策は、単純に 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 に答える