Differently from the case of imperative and functional languages, the research on verification of logic languages, though started since the beginning of logic programming ([10,9,16]), did not result in any widely recognized proof principle or design method (such as, for example, the ones in [14,5,6]), and the field remains still to be explored. The main reason for such a difference can be traced back to an often repeated claim according to which a well-written logic program is ``obviously" correct because it is already a specification of the problem under consideration. This naïve view, originated by the direct use of logic in the programming language, is, however, not applicable even to the pure logic programming paradigm, where programs are sets of definite Horn clauses. In fact, the declarative reading of a pure logic program, that should give its specification, does not always coincide with the procedural one, given in terms of ``computed answer substitutions". As a consequence, whether a program is correct does not derive immediately from its declarative interpretation. When moving to ``real" logic languages like Prolog, the problem is complicated by the extra-logical features of the language which make the declarative nature much more problematic, ([4]). One can easily argue that the case of concurrent logic languages is even more complicated, ([19]). In spite of these considerations, the problem of verifying the correctness of logic programs with respect to a given specification has received its due attention only recently. A survey of the different kinds of proof methods that have been developed for proving declarative properties of definite logic programs can be found in [11,13]. The problem of verification of Prolog programs has been addressed in [4,3,1]. In [2], the influence of the declarative aspect of the logic and Prolog programs on the problem of verification has been pointed out. There have also been attempts to prove properties of general logic programs, i.e. programs in which negative literals can occur in the body of the clauses, ([12,23,29]).
An interesting approach to the problem of verification of logic programs has been proposed by Kanamori and Seki ([21]). It is based on an extension of the Prolog interpreter for Horn clause programs and has been generalized to general logic programs by S. Renault ([29]). The idea of exploiting the interpreter of logic programs (the SLD-resolution or some extension of it) to the purpose of proving properties of the programs themselves, suggested us to have a closer look at the resolution in its guise of theorem prover with the aim of defining more refined and complete formal system that might be relevant to automating the verification process of logic programs.