如何使用Prologs编写定理证明？
我试图将其写为正常，像这样：
parallel(X,Y):-perpendicular(X,Z),perpendicular(Y,Z), X\==Y,!.
perpendicular(X,Y):-perpendicular(X,Z),parallel(Z,Y),!.
你能帮助我吗？
我不愿意发表答案，因为这个问题的框架很糟糕。感谢 theJollySin 添加干净的格式！重写中省略了一些内容，表明了 Aman 的想法，即“I inter in Loop”（原文如此）。
我们不知道输入了什么查询导致了此循环，因此需要进行推测。这两条规则表明 Goal 涉及平行/2或垂直/2谓词。
通过实践，不难理解 Prolog 引擎在提出查询时会做什么，尤其是单目标查询。Prolog 使用非常简单的“跟随你的鼻子”策略来尝试实现目标。查找调用哪个谓词的规则。然后看看是否可以应用这些规则中的任何一个（从第一个规则开始，一直到列表中的规则）。
初级 Prolog 程序员通常会遇到三个主题。一是 Prolog 引擎进行搜索的递归性质。这里， parallel/2的唯一规则有一个右侧，它调用vertical/2的两个子目标，而vertical/2的唯一规则既调用其自身的子目标，又调用parallel/2的另一个子目标。人们应该预料到，试图满足任何一种查询都不可避免地会导致一场类似九头蛇般的两头争斗。
我们在这个例子中看到的第二个主题是自由变量的使用。如果我们要获得有关两条特定线（几何形状）的垂直或平行的知识，那么查询或规则需要以某种方式提供变量与“基础”术语的“绑定”。同样，在没有询问实际目标的情况下，很难猜测阿曼希望其如何发挥作用。也许应该提供有关垂直或平行的特定线的“事实”。行可以仅表示为原子（可能是小写字母），但 Prolog 变量的名称以大写字母（如两个给定规则中所示）或下划线 (_) 字符开头。
最后，第三个可能令人困惑的主题是 Prolog 如何处理否定。这些规则中只有一点点X\==Y被调用。但即使是这个简短的子目标也需要仔细理解。Prolog实现了“否定即失败”，因此X\==Y当且仅当X==Y不成功时才成功。后一个目标也很微妙，因为它询问 和 是否X相同Y，而不尝试进行任何统一。因此，如果这些是不同的变量，并且都是空闲的，那么X==Y就会失败（并且X\==Y成功）。另一方面，X==Y成功（从而X\==Y失败）的唯一方法是两个变量都绑定到相同的基础项。正如上面所讨论的，所述的两个规则没有提供实现这种情况的方法，尽管某些东西可能已经在查询目标中解决了这个问题。
Aman 的家庭作业是了解这些 Prolog 主题：
也许可以对 Prolog 进行几何证明提出更具体的建议！
补充： PTTP（Prolog 技术定理证明器）是由 ME Stickel 在 1980 年代末编写的，这个 2006 年的网页对其进行了描述并提供了下载链接。
它还简洁地总结了为什么 Prolog 本身并不是“一个完整的通用定理证明系统”。也可以在那里跟踪后来的、更有能力的定理证明者。