∃-Universal termination of logic programs

AbstractWe introduce the notion of ∃-universal termination of logic programs. A program P and a goal G ∃-universally terminate iff there exists a selection rule S such that every SLD-derivation of P∪{G} via S is finite. We claim that it is an essential concept for declarative programming, where a crucial point is to associate a terminating control strategy to programs and goals. We show that ∃-universal termination and universal termination via fair selection rules coincide. Then we offer a declarative characterization of ∃-universal termination by defining fair-bounded programs and goals. They provide us with a correct and complete method for proving ∃-universal termination. We show other valuable properties of fair-boundedness, including persistency, modularity, ease of use in paper & pencil proofs, automation of proofs