CW 536

Yi-Dong Shen, Danny De Schreye, and Dean Voets
Termination prediction for general logic programs


We present an approximation framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/non-termination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary queries. We have implemented a termination prediction system and obtained quite satisfactory experimental results. Our prediction is 100% correct for all benchmark programs of the Termination Competition 2007, of which eighteen programs cannot be proved by the existing state-of-the-art analyzers like AProVE07, NTI, Polytool and TALP.

report.pdf (350K) / mailto: D. Voets