Logic Algorithm and Intentions

The idea behind correctness of a logic algorithm wrt its intentions is to state that the intended relation is identical to the relation computed by LA(r)  

Correctness thus states an identity, in the Herbrand models of LA(r), between the intended relation and the interpretation of predicate rin. The second condition, which in general is not a consequence of the first one, is necessary to handle logic algorithms with negation (also see [Deville 90]). 

Since we only consider logic algorithms that are designed by structural induction, correctness reduces, by Corollary 7-1, to = UC r), Moreover, partial correctness is achieved iff UCir) (that is, iff the atoms computed by LA r) are correct), and completeness is achieved iff LA r) (that is, iff all the correct atoms are computed by LA r)). These criteria are in the sequel called the intuitive criteria. 

The total correctness of a logic algorithm wrt its intended relation can however be re-expressed more conveniently, yielding what we call the actual criteria  

We now show that this actual criterion is equivalent to its intuitive counterpart Theorem 7-3 r(X) B[X] is true in5 iff %, = LA r). 

---