{The Iff Proof Procedure for Abductive Logic Programming}