Top-down semantics of fair computations of logic programs

AbstractA successful SLD-derivation from a logic program has as result a positive assertion which is a logical implication of the program regarded as a theory of first-order logic. A finite and failed SLD-tree has as result a negation which is a logical implication of a certain theory which is a strengthened version of the program. In this paper we are concerned with a more general notion of result, one that is applicable to all SLD-derivations, independently of whether they continue on to success, to failure, or whether they are infinite. We discuss the application of our theorem to fair (in the sense of Lassez and Maher) infinite computations