我试着理解公理解析如何在prolog中起作用.
我们假设我在自然数上定义了两个基本运算:
s(term)(代表继任者)和
add(term,anotherTerm).
add的语义由下式给出
add(0,x1) - > x1
add(x1,0) - > x1
add(s(x1),y1) - > s(add(x1,y1))
然后,我想解决这个等式
add(x,add(y,z))= s(0)
我想一个策略可能是
测试方程的右侧(RHS)是否等于其左侧(LHS)
如果没有看到是否可以通过寻找最通用的统一者找到解决方案
如果没有,那么试着找到一个可以在这个等式中使用的公理.做这项工作的策略可能是(对于每个公理):尝试解决等式的RHS等于公理的RHS.如果有解,那么试着求解等式的LHS等于公理的LHS.如果成功,那么我们找到了正确的公理.
最终,如果没有解,并且方程的LHS和RHS是相同的操作(即相同的签名但不是相同的操作数),则对每个操作数应用算法,如果找到每个操作数的解,则找到解.
我认为这个(简单)算法可能有效.但是,我想知道是否有人有解决这类问题的经验？有谁知道我在哪里可以找到一些关于更好算法的文档？
提前致谢