4

我有一个谓词将模态逻辑公式与其负范式联系起来。除了模态运算符、合取和析取之外的所有连接词都被消除了，并且否定被尽可能地推到表达式的叶子中。

rewrite/2✱ 谓词有一个包罗万象的子句，rewrite(A, A).在文本上是 last。有了这个包罗万象的子句，就可以提取否定范式的公式。在这个例子中，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>)总是成功，我不希望它成功。包罗万象的条款真的应该是一个包罗万象的条款，而不是如果另一个条款适用的话可能会触发的东西。

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

如果您使用干净的数据表示，这些问题都会消失。

在这种情况下，这意味着您将完全类似于您如何通过不同的函子系统地表示所有其他实体，也应使用专用函子来表示（模态）变量。

例如，让我们使用函子v/1来表示变量。这意味着我们使用v(1)等v(7)来表示模态变量 1、7 等。

我添加了以下子句，而不是您的“catch all”子句，这些子句说明了模态变量的含义：

%（否定）变量

重写（n（v（V）），n（v（V）））。
重写（v（V），v（V））。

现在我们得到：

?-重写（e（v（4），v（7）），Z）。
Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7))))。

请注意，我们当然必须v/1在查询中使用包装器，并在答案中获取包装器。这比不存在包装器时稍微难读和写。但是，它使对此类公式的推理变得更加容易，因此我强烈建议使用它。

在这些公式和您当前使用的默认表示之间进行转换是一个简单的练习。它之所以被称为“defaulty”，正是因为它需要一个默认（“catch all”）案例，也因为它被认为是错误的。最好尽快摆脱此类表示，然后围绕干净的表示编写主要逻辑。

干净的表示有利于通用性，也有利于提高效率：您的 Prolog 系统的参数索引现在可以通过第一个参数的主函子轻松区分所有子句，这提高了该参数被完全实例化的重要用例的性能（例如，在您发布的示例中）。

于 2018-12-15T10:43:23.223 回答