prolog - 如何确定两个命题公式在 Prolog 中是否等价？

Question

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

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

我知道两个命题等价如果

重言式 (A iff 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 → B ∧ B → A 是等价的持有。如果你能证明这个公式，你就完成了。

现在是序言部分:

• 您混淆了谓词和术语级别:and(A, B)将失败并显示错误消息 A没有充分实例化。创建谓词要容易得多eval并定义 eval(and(A,B)) , eval(or(A,B))等
• 您没有逻辑变量的表示。假设我的公式是 A .我如何知道 A可能是真/假？我建议将变量显式包装到构造函数中 var(Truthvalue)在模式匹配过程中将其与逻辑运算符区分开来。否则，您的证明搜索将尝试将变量扩展为更复杂的公式，这显然没有帮助。
• 在不必要的地方使用 cuts/fail:and(P,Q) 只有一个定义这样切割就不会做任何事情。类似地，fail 使规则失败，就好像它不存在一样 - 因此您可以删除这些规则(除非您使用 cut 的额外功能，即)。请记住，cut 的行为不像逻辑结构，应尽可能避免。
• 你在制定否定时遇到了问题:你没有明确的否定规则，你的 ⊤ 和 ⊥ 谓词与你的其余规则没有联系(假设你想将 ¬A 定义为 A → ⊥)。这是由于 Prolog 规则的不对称性:推导谓词意味着它是真的，但不可推导性不是定义逻辑错误陈述的好方法。在这种情况下，我们可以明确说明公式为假的含义:例如A ∧ B如果 A 则为假为假或 B是错误的(或两者)。让我们分开eval然后分为两部分:eval_tt(X)可推导的是如果X是真的 eval_ff(X)如果 X 是可推导的是假的。

将所有这些笔记放在一起，这就是 ∧ 和 ¬ 的最小完整微积分:

eval_tt(var(true)).
eval_tt(and(A,B)) :-
    eval_tt(A),
    eval_tt(B).
eval_tt(not(A)) :-
    eval_ff(A).


eval_ff(var(false)).
eval_ff(and(A,_B)) :-
    eval_ff(A).
eval_ff(and(_A,B)) :-
    eval_ff(B).
eval_ff(not(A)) :-
    eval_tt(A).

我们可以查询 ¬(A ∧ ¬B) 的模型与查询:

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

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

还有 A ∧ ¬A正如预期的那样是不可满足的:

?- eval_tt(and(var(A), not(var(A)))).
false.

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

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

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

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

?- valid2(not(and(var(X),not(var(X))))).
true.

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

?- valid(X).
false.

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