In:
Theory and Practice of Logic Programming, Cambridge University Press (CUP), Vol. 10, No. 4-6 ( 2010-07), p. 365-381
Abstract:
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.
Type of Medium:
Online Resource
ISSN:
1471-0684
,
1475-3081
DOI:
10.1017/S1471068410000165
Language:
English
Publisher:
Cambridge University Press (CUP)
Publication Date:
2010
detail.hit.zdb_id:
2045489-2
Permalink