prolog捕获只有在没有其他子句时才有效的所有子句

我有一个谓词,它把模态逻辑公式和它的负正规形式联系起来。除模态运算符、连词和析取之外的所有连接词都将被消除,并且将否定尽可能地推送到表达式的叶中。

这个 rewrite/2 _谓词有一个catch all子句 rewrite(A, A). 那就是 最后一个文本 . 有了这个catch all子句,就有可能提取出一个形式为负正规的公式。在这个例子中, e 是“Ukasiewicz”符号中的双条件连接,并且 4 和 7 是模态逻辑中的变量(因此是prolog常量)。

Z 与负正规形式的公式统一。

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

然而, rewrite(<some constant>, <some constant>) 总是成功的,我不想成功。catch all子句实际上应该是catch all,而不是在另一个子句适用时可能激发的内容。

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

我试图替换 重写(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不是由具有特殊含义的Atom/构造函数领导的。然而,在做出这种改变之后, rewrite 如果递归调用,则始终失败。

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

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

设置catch all子句的正确方法是什么?

_?供参考的程序全文:

% 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).