SLD resolution

SLD resolution, or **Selective Linear Definite clause resolution**, is a key concept in the field of logic programming and automated theorem proving. It is a refinement of the resolution principle that is used to infer conclusions from a set of logical clauses. SLD resolution specifically applies to definite clauses, which are expressions in propositional logic or predicate logic that have a specific format.