Termination Prediction for General Logic Programs

The authors present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/non-termination proof approaches. They 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. They 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 non-floundering queries. They have implemented a termination prediction tool and obtained quite satisfactory experimental results.