Prolog解析证明器删除括号

Posted 2023-05-08

【中文标题】Prolog解析证明器删除括号

【英文标题】：Prolog resolution prover deletes brackets

【发布时间】：2020-08-24 07:36:33

【问题描述】：

我正在用 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 and b 周围的括号已被删除，而它们仍保留在第一个子句中。为什么会这样？

作为参考，this 是我的代码，给出该输出的命令是 singlestep([[(a and b) equiv c]], X). 应该如何处理 equiv 的具体代码在第 93 行，函数 singlestep 在第 108 行。

【问题讨论】：

这可能是因为您在运算符中定义的优先级，因为那时这些括号是多余的。

所有运算符的优先级相同，除了neg 更高。那么当运算符具有相同的优先级时，肯定需要括号吗？

好吧，右边是从左到右的，所以(((neg c) or a) and b)。

@WillemVanOnsem：我认为您的评论在技术上有点不正确。当我查询F=(neg c or a and b), F =.. G 时，我得到G = [or, neg c, a and b] 的结果。因此，带括号的表达式是(neg c) or (a and b)。因此，Nathan 的代码似乎是正确的。一般来说，如果你使用 Prolog 操作符，Prolog 系统会关心括号。

@tphilipp: arrghh 是的，它朝相反的方向发展，抱歉，不知何故弄混了。谢谢。

【参考方案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.

确认如何解释运算符。