5

特定の入力が数式を表しているかどうかを検証するために、述語を作成しようとしています。

p、q、r、s、t などの命題アトムにのみ使用することが許可されています。テストする式は次のとおりです。

neg(X) - represents the negation of X  
and(X, Y) - represents X and Y  
or(X, Y) - represents X or Y  
imp(X, Y) - represents X implies Y

wff与えられた構造が式の場合に true を返し、それ以外の場合に false を返す述語を作成しました。また、数式内で変数を使用する必要はありません。以下で説明するように、命題アトムのみを使用します。

logical_atom( A ) :-
    atom( A ),     
    atom_codes( A, [AH|_] ),
    AH >= 97,
    AH =< 122.

wff(A):-
    \+ ground(A),
    !,
    fail.

wff(and(A, B)):-
    wff(A),
    wff(B).

wff(neg(A)):-
    wff(A).

wff(or(A, B)):-
    wff(A),
    wff(B).

wff(imp(A, B)):-
    wff(A),
    wff(B).

wff(A):-
    ground(A),
    logical_atom(A),
    !.

このようなテストを導入する wff(and(q, imp(or(p, q), neg(p)))).と、呼び出しは と の両方の値を返しtrueますfalse。なぜこのようなことが起こるのか教えてください。

4

1 に答える 1

11

式を表すために選択したデータ構造は、「デフォルト」と呼ばれます。これは、アトミック識別子をテストするために「デフォルト」のケースが必要なためです。上記のいずれでもないもの（および、または、neg、imp）で、logical_atom/1を満たすものすべては論理アトムです（あなたの表現では）。インタプリタは、これらのケースをファンクタで区別して、最初の引数のインデックスを適用することはできません。および/または/etc。と同様に、アトミック変数に専用のファンクター、たとえば「atom（...）」を装備する方がはるかにクリーンです。wff/1は次のように読み取ることができます。

wff(atom(_)).
wff(and(A, B))    :- wff(A), wff(B).
wff(neg(A))       :- wff(A).
wff(or(A, B))     :- wff(A), wff(B).
wff(imp(A, B))    :- wff(A), wff(B).

これで、クエリは必要に応じて決定論的になります。

?- wff(and(atom(q), imp(or(atom(p), atom(q)), neg(atom(p))))).
true.

数式が最初にこのように表現されていない場合は、最初に数式をそのような形式に変換してから、デフォルトではない表現を使用してさらに処理することをお勧めします。

追加の利点は、次のようなコードを使用して、簡単にテストするだけでなく、整形式の数式を列挙できることです。

wff(atom(_))  --> [].
wff(and(A,B)) --> [_,_], wff(A), wff(B).
wff(neg(A))   --> [_], wff(A).
wff(or(A,B))  --> [_,_], wff(A), wff(B).
wff(imp(A,B)) --> [_,_], wff(A), wff(B).

そして、次のようなクエリ：

?- length(Ls, _), phrase(wff(W), Ls), writeln(W), false.

降伏：

atom(_G490)
neg(atom(_G495))
and(atom(_G499),atom(_G501))
neg(neg(atom(_G500)))
or(atom(_G499),atom(_G501))
imp(atom(_G499),atom(_G501))
and(atom(_G502),neg(atom(_G506)))
and(neg(atom(_G504)),atom(_G506))
neg(and(atom(_G504),atom(_G506)))
neg(neg(neg(atom(_G505))))
neg(or(atom(_G504),atom(_G506)))
neg(imp(atom(_G504),atom(_G506)))
etc.

その出力として。

于 2010-10-16T10:21:10.543 に答える