5

如何使用 Prologs 编写定理证明？

我试着把它写成正常的像这样：

parallel(X,Y):-perpendicular(X,Z),perpendicular(Y,Z), X\==Y,!.
perpendicular(X,Y):-perpendicular(X,Z),parallel(Z,Y),!.

你能帮助我吗？

4

1 回答 1

4

我不愿意发布答案，因为这个问题的框架很差。感谢 theJollySin 添加了干净的格式！重写中省略了一些东西，表明 Aman 的想法是“I inter in Loop”（原文如此）。

我们不知道输入了什么查询导致了这个循环，所以需要推测。这两条规则表明 Goal 涉及parallel/2或vertical/2谓词。

通过实践，不难理解 Prolog 引擎在提出查询时会做什么，尤其是单目标查询。Prolog 使用一个非常简单的“跟随你的鼻子”策略来尝试实现一个目标。查找调用谓词的规则。然后看看是否可以应用这些规则中的任何一个，从第一个开始并在它们的列表中向下。

Prolog 初学者通常会遇到三个问题。一是 Prolog 引擎进行搜索的递归性质。在这里， parallel/2的唯一规则有一个右侧调用两个子目标的垂直/2，而垂直/2 的唯一规则调用它自己的一个子目标和另一个并行/2的子目标。人们应该预料到，试图满足任何一种查询都不可避免地会导致与分叉头的类似九头蛇的斗争。

我们在这个例子中看到的第二个主题是自由变量的使用。如果我们要获得关于两条特定线（几何）的垂直性或平行性的知识，那么查询或规则需要以某种方式将变量“绑定”到“基础”术语。同样，如果没有查询实际的目标，很难猜测 Aman 期望它如何工作。也许应该提供有关垂直或平行的特定线的“事实”。行可以仅表示为原子（可能是小写字母），但 Prolog 变量是以大写字母（如在两个给定规则中）或下划线 (_) 字符开头的名称。

最后，可能相当混乱的第三个主题是 Prolog 如何处理否定。这些规则中只有一点点，X\==Y调用的地方。但即使是这个简短的子目标也需要仔细理解。Prolog 实现了“否定为失败”，因此X\==Y当且仅当不成功时才X==Y成功。后一个目标也很微妙，因为它询问是否相同X，Y而不试图进行任何统一。因此，如果这些是不同的变量，都是自由的，那么X==Y就会失败（并且X\==Y成功）。另一方面，X==Y成功的唯一途径（因此X\==Y失败）将是如果两个变量都绑定到相同的基本项。正如上面所讨论的，上述两条规则并没有为这种情况提供一种方法，尽管在查询目标中可能已经解决了这个问题。

Aman 的家庭作业是了解这些 Prolog 主题：

  • 递归
  • 自由和绑定变量
  • 否定

也许可以就 Prolog 做几何证明提出更具体的建议！

补充： PTTP（Prolog Technology Theorem Prover）是由 ME Stickel 在 1980 年代后期编写的，这个 2006 年的网页描述了它并提供了下载链接。

它还简洁地总结了为什么单独的 Prolog 不是“一个完整的通用定理证明系统”。指向后来的更强大的定理证明者的指针也可以在那里遵循。

于 2012-04-18T15:37:20.410 回答