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的正字詞相統一，那么它就是一個失敗的結點。