| Autor: |
Yi-Dong Shen, de Schreye, Danny, Voets, Dean |
| Předmět: |
|
| Zdroj: |
Theory & Practice of Logic Programming; Nov2009, Vol. 9 Issue 6, p751-780, 30p |
| Abstrakt: |
We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination 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 nonfloundering queries. We have implemented a termination prediction tool and obtained quite satisfactory experimental results. Except for five programs which break the experiment time limit, our prediction is 100% correct for all 296 benchmark programs of the Termination Competition 2007, of which 18 programs cannot be proved by any of the existing state-of-the-art analyzers like AProVE07, NTI, Polytool, and TALP. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
