Automated termination analysis for logic programs with cut

作者：Schneider Kamp Peter^*; Giesl Juergen; Stroeder Thomas; Serebrenik Alexander; Thiemann Rene

来源：Theory and Practice of Logic Programming, 2010, 10: 365-381.

DOI：10.1017/S1471068410000165

• automated termination analysis
• cut
• definite logic programs

Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing in our termination prover AProVE and evaluated it successfully with extensive experiments.

• 出版日期2010-7