Finite failure is and-compositional

We study some properties of SLD-trees related to finite failure. The main results are a theorem stating that the non-ground finite failure set is a correct and fully abstract semantics wrt finite failure and a second theorem stating that the complement of non-ground finite failure is and-compositional, i.e. that the finite failure behaviour of conjunctive goals can be derived from the finite failure behaviour of atomic goals. The proofs are based on two new lemmata which generalize to infinite derivations theorems which are valid for successful and finitely failed derivations.