Finite failure is and-compositional
Roberta Gori · Journal of Logic and Computation · 1997
We study some properties of SLD-trees related to nite failure. The main results are a theorem stating that the non-ground nite failure set is a correct and fully abstract semantics wrt nite failure and a second theorem stating that the complement of non ground nite failure is andcompositional, i.e. that the nite failure behaviour of conjunctive goals can be derived from the nite failure behaviour of atomic goals. The proofs are based on two new lemmata which generalize to innite derivations theorems which are valid for successful and nitely failed derivations. 1 Introduction The operational semantics of (positive) logic programs is usually based on SLDtrees. Several operational properties, useful for reasoning about programs, can be extracted from an SLD-tree. Examples are SLD-derivations, resultants, partial answers, computed answers, nite failures. All these properties, that we call observables, can be obtained as abstractions of the SLD-tree. The study of the obser...