SLD resolution

SLD resolution (Selective Linear Definite clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.

Given a goal clause:

${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$

with selected literal ${\displaystyle \neg L_{i}}$, and an input definite clause:

${\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}$

...
Wikipedia