Encoding of SLD-resolution

 

  

Figure: Our encoding of SLD-resolution

  

Figure: a normal form

In this subsection, we show a translation from a logic programming language based on SLD resolution with the same strategy as PROLOG. We assume that readers are familiar with SLD-resolution. A suitable reference is [Llo87]. Figure  shows the translation of program clauses and the translation of goal clauses, where X₁,...,X_n in RESULT_n(X₁,...,X_n) are all the variables that are included in a goal g(t₁),...,g(t_m) . When a translated net become a normal form of Figure , the original goal is regarded as successful and then one of the solutions is [s₁/X₁,...,s_n/X_n] .

Theorem 1

Let P be a set of clauses and g be a goal in SLD-resolution. g has a computed answer q under P iff the translated net of g has the solution q under the translated rewrite rules of P .

Proof. -if part is shown by on the length of SLD-resolution and If-part by induction on the length of reduction of additive interaction nets.

The above encoding of SLD-resolution does not implement the behavior of PROLOG completely, which is the same as the description of SLD-resolution in [Llo87], because rewrite rules which have redexes with the same agent name are applied to goals arbitrarily. But it is certainly possible that we give a priority order on rewrite rules with the same agent name to simulate the PROLOG implementation.