In the rest of this section we assume all the traditional definitions of mathematical logic .
Logic Programming  is a well-known programming paradigm based on a subset of First Order Logic--named Horn Clause Logic. A program is composed by a set of clauses (i.e., implications) of the form and execution is driven by a query (or goal) of the form .
Given a program P and a query , the purpose of an execution is to verify under which conditions the conjunction is a logical consequence of the program P--i.e., .
The computation process is based on two basic mechanisms, mainly due to Robinson , namely Resolution and Unification. Unification of two atoms A and B is the process of computing a substitution such that .
During resolution, given a query , a literal is selected, and a clause such that H and unify is used to produce a new query (named resolvent)
where is the (most general) unifier of H and .
In general, no restrictions are imposed on the order in which the subgoals and the clauses to be used are selected--i.e., they are non-deterministic operations. In particular:
Different languages and different semantics can be obtained by playing on the definition of these two selection operations (i.e. subgoal selection and clause selection).
Prolog  is the most popular logic programming language. Prolog is based on Horn Clause Logic and its semantics are based on the previously described resolution + unification mechanisms. Prolog's operational semantics define the two select operations as follows:
Prolog extends pure Horn clause logic with some additional features, aimed at making Prolog a ``complete'' programming language. The most relevant extensions are:
The semantics of Prolog are heavily based on the ordering adopted by the two selection functions--which is fundamental for the correct behaviour of the various extra-logical features of the language. From now on, whenever we talk about Prolog semantics we refer to this ordering of exploration of the search space. Because of this, we will often refer to those extra-logical predicates whose behaviour depends on their order of execution as order-sensitive predicates.