Prolog中如何判断两个命题公式是否等价？

Question

我是 Prolog 新手，有一些疑问。

我需要编写一个函数 form_equiv(A,B) 来告诉我们 B 是否等于 A，其中 A 和 B 应该是命题。

我知道两个命题是等价的，如果

同义反复 (A 当且仅当 B) = TRUE

但是我怎样才能创建一个函数来检查公式何时是同义反复。

顺便说一句，我不能仅使用内置函数 AND、OR 和 NOT。

现在这是我到目前为止所拥有的：

and(P,Q) :- P, Q, !.
or(P,Q) :- (P; Q), !.
impl(P,Q) :- or(not(P),Q).
syss(P,Q) :- and(impl(P,Q),impl(Q,P)).

t.
f :- fail.

t(_).
f(_) :- fail.



:- op(400,xf,not).
:- op(500,xfx,and).
:- op(500,xfx,or).
:- op(600,xfx,impl).
:- op(700,xfx,syss).

我在 Haskell 中完成了一个类似的程序，但我对 Prolog 真的很陌生。

谁能帮我写一个函数来检查公式是否是同义反复？

提前致谢...

Answer 1

首先是逻辑部分：两个公式A和B如果A \xe2\x86\x92 B \xe2\x88\xa7 B \xe2\x86\x92 A成立则等价。如果你能证明这个公式，你就完成了。

\n

现在到序言部分：

\n

\n
• 您混淆了谓词和术语 level: will 失败，并显示未充分实例化的and(A, B)错误消息。A创建谓词eval并定义要容易得多eval(and(A,B))，eval(or(A,B))等要容易得多。
\n
• 您没有逻辑变量的表示。假设我的公式只是A. 我如何知道是否A可以接受真/假？我建议将变量显式包装到构造函数中var(Truthvalue)，以在模式匹配期间将其与逻辑运算符区分开来。否则，您的证明搜索将尝试将变量扩展为更复杂的公式，这显然没有帮助。
\n
• 您可以在不必要的地方使用“cuts/fail”：只有一个and(P,Q)这样的定义，即“cut”不会执行任何操作。类似地，失败会使规则失败，就好像它不存在一样 - 因此您可以删除这些规则（除非您使用 cut 的额外逻辑功能）。请记住，剪切的行为不像逻辑结构，应尽可能避免。
\n
• 您在制定否定时遇到问题：您没有明确的否定规则，并且 \xe2\x8a\xa4 和 \xe2\x8a\xa5 的谓词未连接到其余规则（假设您想定义 \xc2\xacA为 A \xe2\x86\x92 \xe2\x8a\xa5)。这是由于 Prolog 规则的不对称性造成的：推导谓词意味着它是真的，但不可推导性并不是定义逻辑错误语句的好方法。在这种情况下，我们可以明确说明公式为假的含义：例如，A \xe2\x88\xa7 B如果A为假或B为假（或两者），则为假。让我们分成eval两部分：eval_tt(X)如果为X真则可导，eval_ff(X)如果为假则可导X。
\n

\n

将所有这些注释放在一起，这就是 \xe2\x88\xa7 和 \xc2\xac 的最小完整演算：

\n

eval_tt(var(true)).\neval_tt(and(A,B)) :-\n    eval_tt(A),\n    eval_tt(B).\neval_tt(not(A)) :-\n    eval_ff(A).\n\n\neval_ff(var(false)).\neval_ff(and(A,_B)) :-\n    eval_ff(A).\neval_ff(and(_A,B)) :-\n    eval_ff(B).\neval_ff(not(A)) :-\n    eval_tt(A).\n

\n

\xc2\xac(A \xe2\x88\xa7 \xc2\xacB)我们可以使用以下查询来查询模型：

\n

?- eval_tt(not(and(var(A), not(var(B))))).\nA = false ;\nB = true.\n

\n

如果我们使用剪切或否定作为失败，我们可能不会找到这两种解决方案。

\n

正如A \xe2\x88\xa7 \xc2\xacA预期的那样，也是不满意的：

\n

?- eval_tt(and(var(A), not(var(A)))).\nfalse.\n

\n

现在您只需要通过您想要的其他运算符（析取、蕴涵、等价等）来扩展这个最小微积分。顺便提一句。如果您看过序列微积分，您可能会认识到其中的一些想法:)

\n

编辑：我还没有解释如何从可满足性到有效性。问题如下：从查询到的答案替换eval_tt(X)仅告诉我们这X是可以满足的。在逻辑上，我们通常将 X 定义为有效，因为 \xc2\xacX 是不可满足的。这可以在 Prolog 中通过定义将否定表示为失败：

\n

valid(X) :-\n  \\+ eval_ff(X).\n

\n

这里有什么问题？我们检查可满足性的公式，例如

\n

?- valid2(not(and(var(X),not(var(X))))).\ntrue.\n

\n

但我们没有得到答案替换。特别是如果查询没有充分实例化，我们会得到错误的结果：

\n

?- valid(X).\nfalse.\n

\n

但肯定有一个有效的公式——我们在上面尝试过一个。我还没有找到一个可以枚举所有有效公式的好的解决方案。

\n