
## Definition: Reduction

A reduction of goal G by a program P is the replacement of G by the body of an instance of a clause in P, 
whose head is identical to the chosen goal. Example: the goal grandparent(abraham, X)? Can be reduced to parent (abraham, Y), parent(Y, X) 
with respect to the clause : grandparent(Z, X) Å parent (Z, Y), parent(Y, X). 

Definition: Variables quantification Variables in queries are *existentially* quantified, while in facts are *universally* quantified. A query p(T1,T2,…,Tn)? , which contain the variables X1,X2, ..., Xk reads: 
"Are there X1,X2, ..., Xk such that p(T1,T2,..., Tn)? " usually, existential quantification is usually omitted. 

Example: the query father (abraham, X)? reads : 
"Does there exist an X such that abraham is the father of X ? " 
A fact p(T1,T2,…,Tn) reads : "For all X1,X2, ..., Xk ,where Xi are the variables occurring in the fact p(T1,T2,..., 
Tn) , is true ". Logically, from a universally quantified fact one can deduce any instance of it. 

Example: From likes(X, apple) , deduce likes (abraham, apple) 

## Definition: Most General Unifier (Mgu)

A unifier of two terms is a substitution making the terms identical. If two terms have a unifier, we say they unify. MGU of two terms is a unifier such that the associated common instance is most general. If two terms unify, all MGUs are equivalent. 

## Definition: Computation

a computation of a goal Q= Q0 by a program P is a sequence of triples (Qi, Gi, Ci) . 

where : Qi is a conjunctive goal, Gi is a goal occurring in Qi, and Ci is a clause AÅB1,…, Bk in P, that contains new variables not occurring in Qj, 0≤j≤i. 

For a detailed introductory discussion please refer to ([Sterling& Shapiro 1994] and [Bochman1998]). 

## 4.Semantics Of Logic Programs

A logic program can have many semantics according the point of view. The common semantics are operational, denotational, and declarative. The operational semantics of logic programs are considered a way of describing the meaning of the programs procedurally. It is a set of ground goals that are instances of queries solved by a logic program P using abstract interpretation as shown in section 4.1. The declarative semantics of logic programs are derived from the term model, referred to as the Herbrand base. The declarative semantics is discussed in section 4.2. The denotational semantics of logic programs are defined in terms of a function which assigns meaning to the program. The function is over the domain computed by the program. Meaning is defined as the least fixpoint of the function, if it exists. The denotational semantics is out of concern of this paper, since Kowalski's famous slogan "Algorithms= Logic + Control" [Kowalski1979] implies that declarative logic statements can be interpreted as procedural computer instructions. We presume that declarative and operational semantics are sufficient to reflect the algorithm of a logic program. 

## 4.1. Interpreting Logic Programs

In the next, we show the algorithm of an abstract interpreter for logic programs. It is used to construct the operational semantics for a logic program. Note that this algorithm depends on **unify** function which is mentioned in line 5. This function is defined by the Unification algorithm. 

## Abstract Interpreter For Logic Programs Input: A Goal G And A Program P

Output: an instance of G that is a logical consequence of P, or no otherwise. Algorithm: 
1 2 3 4 5 6 7 8 9 initialize the resolvent to G. while the resolvent is not empty do choose a goal A from the resolvent choose a (renamed) clause A' Å B1, …, Bn from P 
 such that A and A' **unify** with MGU Θ. 

 (if no such goal and clause exist, exit the while loop) 
 replace A by B1, …, Bn in the resolvent apply Θ to the resolvent and to G 
 if the resolvent is empty, then output G, else output no. 