Selective Linear Definite Clause Resolution is an inference rule used in logic programming, often known as SLD resolution. It refines resolution for Horn clauses and provides a formal basis for query evaluation in languages such as Prolog.
(Also simply SLD resolution.) The basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.