首先是逻辑部分：如果成立，两个公式A和B等价。A → B ∧ B → A如果你能证明这个公式，你就完成了。
现在到序言部分：
- 您正在混淆谓词和术语级别：将失败并显示未充分实例化
and(A, B)的错误消息。创建谓词和定义,等A要容易得多。evaleval(and(A,B))eval(or(A,B))
- 您没有逻辑变量的表示。说我的公式只是
A。我如何确定是否A可以接受真/假？我建议将变量显式包装到 aa 构造函数var(Truthvalue)中，以在模式匹配期间将其与逻辑运算符区分开来。否则，您的证明搜索将尝试将变量扩展为更复杂的公式，这显然没有帮助。
- 您在不必要的地方使用 cut / fail：只有一个定义
and(P,Q)使得 cut 不做任何事情。同样，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.
但肯定有一个有效的公式 - 我们在上面尝试了一个。我还没有找到一个可以枚举所有有效公式的好解决方案。