K. R.  Apt and Pedreschi, D., ?Proving Termination of General Prolog Programs?, in TACS, 1991, pp. 265-289.