SLD解析

SLD解析是逻辑编程中使用的基本推理规则。它是对解析的细化，对于霍恩子句来说，它既是健全的，又是反驳完整的。

给定一个目标句，表示为要解决的问题的否定。SLD解析得出另一个目标句，其中所选字词被输入句子的否定字词所取代。SLD解析得出另一个目标句，其中所选字词被输入句的否定字词和统一替换所取代

它的名字来自于SL解析，对于逻辑的非限制性条款形式来说，SL解析既是健全的，又是完全的反驳。SLD是指有确定条款的SL解析。在SL和SLD中，L代表决议证明可以被限制在条款的线性序列中。在SLD中，序列中的所有子句都是目标子句，而另一个父句是一个输入子句。在SL解析中，另一个父句要么是输入句，要么是序列中较早的一个祖先句。在SL和SLD中，S代表了这样一个事实：在任何子句中xxx被解决的字词是xxx被选中的字词。是由选择规则或选择函数xxx选择的。在SL解析中，被选择的字词被限制为最近被引入到子句中的字词。在最简单的情况下，这种后进先出的选择函数可以由字词的书写顺序指定，就像在Prolog中一样。然而，SLD解析中的选择功能比SL解析和Prolog中的更普遍。对于可以被选择的字词没有任何限制。

在条款逻辑中，SLD反驳证明了输入的条款集是不可满足的。然而，在逻辑编程中，SLD反驳也有一个计算性的解释。是通过反向推理的方式，用一个输入句子作为目标还原，推导出一组新的子目标。是指通过逆向推理，用一个输入句子作为目标还原过程，推导出一组新的子目标。统一替换既把输入从选定的子目标传递给程序的主体，同时又把输出从程序的头部传递给其余未选定的子目标。

SLD解析隐含地定义了一棵替代计算的搜索树，其中初始目标子句与树的根相关。对于树上的每一个节点和程序中的每一个定语从句，其正字与与该节点相关的目标从句中的选定字统一，有一个子节点与通过SLD解析得到的目标从句相关。一个没有子节点的叶子节点是一个成功的节点，如果它的相关目标条款是空条款。如果它的相关目标子句是非空的，但是它所选择的字词没有与SLD的正字词相统一，那么它就是一个失败的结点。