syntax - Prolog resolution prover 删除括号

Question

我正在用 prolog 编写分辨率证明程序，它接受以下形式的输入

[[(a or b) equiv neg(c and d)]]

等，并将它们转换为 CNF。所有逻辑运算符都可以正常工作，但是当程序尝试扩展 equiv 运算时，括号会丢失。例如，在

上执行算法的一个步骤

[[(a and b) equiv c]]

给出结果

[[neg(a and b) or c], [neg c or a and b]]

在第二个子句中，a 和 b 两边的括号已被删除，而它们保留在第一个子句中。为什么会这样？

供引用，this是我的代码，给出输出的命令是 singlestep([[(a and b) equiv c]], X). 应该如何处理 equiv with 在第 93 行，函数 singlestep 在第 108 行。

Answer 1

发生这种情况是因为运算符优先级的定义方式是

neg c or (a and b)

和

neg c or a and b

是等价的。您没有包含您的运算符声明，但它们很可能都是具有相同优先级的 xfy。

要测试等价性，您可以尝试简单的模式匹配:

?- neg c or a and b = X or Y.
X = neg c,
Y = a and b?

?- neg c or a and b = X and Y.
no.

确认运算符的解释方式。