4

様相論理式をその負の正規形に関連付ける述語があります。様相演算子、接続詞、および論理和を除くすべての接続詞は削除され、否定は可能な限り式のリーフに押し込まれます。

✱述語には、テキスト上は lastrewrite/2であるキャッチオール句rewrite(A, A).があります。このキャッチオール句を使用すると、式を否定された正規形で抽出できます。この例では、 はŁukasiewicz 記法のような二条件接続詞であり、とは様相論理の変数 (つまり Prolog 定数) です。e47

Z負の正規形の式で統一されます。

?- rewrite(e(4, 7), Z).
Z = a(k(4, 7), k(n(4), n(7)))

ただし、rewrite(<some constant>, <some constant>)常に成功し、成功しないようにしたいと思います。キャッチオール句は、別の句が適用可能な場合に発生する可能性があるものではなく、キャッチオールであるべきです。

?- rewrite(e(4, 7), e(4, 7)).
true.

rewrite(A, A).を保護されたバージョンに置き換えてみました：

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

rewrite(A, A) :- \+ wff_shallowly(A).

これにより、 A が特別な意味を持つアトム/コンストラクターによって先頭にない場合にのみ、キャッチオール句が適用されなくなると思いました。ただし、その変更を行った後、rewrite再帰的に呼び出すと、常に失敗します。

?- rewrite(4, Z).
Z = 4.

?- rewrite(c(4, 7), Z).
false.

キャッチオール句を設定する正しい方法は何ですか?

✱ 参考のためのプログラムの全文:

% so the primitive connectives are
% l <-- necessity
% m <-- possibility
% c <-- implication
% f <-- falsehood
% t <-- truth
% k <-- conjunction
% a <-- alternative
% n <-- negation
% e <-- biconditional

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

% falsehood is primitive
rewrite(f, f).

% truth is primitive
rewrite(t, t).

% positive connectives
rewrite(a(A, B), a(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(k(A, B), k(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(l(A), l(C)) :- rewrite(A, C).
rewrite(m(A), m(C)) :- rewrite(A, C).

% implication
rewrite(c(A, B), a(NC, D)) :-
  rewrite(n(A), NC), rewrite(B, D).

% biconditional
rewrite(e(A, B), a(k(C, D), k(NC, ND))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated falsehood is truth
rewrite(n(f), t).

% negated truth is falsehood
rewrite(n(t), f).

% double negation elimination
rewrite(n(n(A)), C) :- rewrite(A, C).

% negated alternation
rewrite(n(a(A, B)), k(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated conjunction
rewrite(n(k(A, B)), a(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated biconditional
rewrite(n(e(A, B)), a(k(C, ND), k(NC, D))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated necessity
rewrite(n(l(A)), m(NC)) :- rewrite(n(A), NC).

% negated possibility
rewrite(n(m(A)), l(NC)) :- rewrite(n(A), NC).

% catch all, rewrite to self
rewrite(A, A) :- \+ wff_shallowly(A).
4

1 に答える 1

5

データのクリーンな表現を使用すると、これらの問題はすべて解消されます。

この場合、他のすべてのエンティティをさまざまな functorを介して体系的に表す方法と完全に類似して、専用の functor を使用して (モーダル)変数を表す必要があることを意味します。

たとえば、ファンクターv/1を使用して変数を表現してみましょう。これは、モーダル変数 1、7 などを表すためv(1)になどを使用することを意味します。v(7)

「キャッチオール」句の代わりに、モーダル変数について何が保持されるかを述べる次の句を追加します。

% (否定) 変数

rewrite(n(v(V)), n(v(V)))。
rewrite(v(V), v(V))。

今、私たちは得ます：

?- rewrite(e(v(4), v(7)), Z)。
Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7))))。

v/1もちろん、クエリでラッパーを使用し、回答でラッパーを取得する必要があることに注意してください。これは、ラッパーが存在しない場合よりも読み書きが少し難しくなります。ただし、そのような式についての推論がはるかに簡単になるため、使用することを強くお勧めします.

そのような式と現在使用しているデフォルトの表現との間で変換するのは簡単な作業です。これは、デフォルト(「すべてをキャッチ」) のケースが必要であり、それがfaultyと見なされるため、まさに「defaulty」と呼ばれます。そのような表現をできるだけ早く取り除き、クリーンな表現の周りにメイン ロジックを記述することをお勧めします。

きれいな表現は、一般性にも効率にも適しています: Prolog システムの引数のインデックス付けは、最初の引数のプリンシパル ファンクターを介してすべての句を容易に区別できるようになりました。これにより、その引数が完全にインスタンス化される重要なユース ケースでのパフォーマンスが向上します (たとえば、投稿した例では）。

于 2018-12-15T10:43:23.223 に答える