我试图理解公理解析在PROlog中是如何工作的。
假设我定义了自然数的两个基本运算：
s（term）（代表继任者）和
添加（术语，另一术语）。
add的语义由
加（0，x1）—>x1
加（x1，0）—>x1
加法（x1，y1）－>s（加法（x1，y1））
那么，我想解这个方程
加（x，加（y，z））=s（0）
我想一个策略是
测试方程式的右侧（Rhs）是否等于其左侧（Lhs）
如果不知道是否可以通过寻找最通用的统一器来找到解决方案
如果没有，那么尝试找到一个公理，可以在这个方程式中使用。做这项工作的策略可以是（对于每一个公理）：尝试求解等式的RHS等于公理的RHS。如果有一个解决方案，那么尝试求解等式的LHS等于公理的LHS。如果它成功了，我们就找到了正确的公理。
最后，如果没有解，且方程的lhs和rhs是相同的运算（即相同的签名但不同的操作数），则对每个操作数应用该算法，如果找到每个操作数的解，则找到一个解。
我认为这个（简单的）算法可能有用。
但是，我想知道是否有人有解决此类问题的经验？
有人知道我在哪里可以找到更好算法的文档吗？
提前谢谢
最佳答案