Automated termination analysis for logic programs with cut

P. Schneider-Kamp, J. Giesl, T. Stroeder, A. Serebrenik, R. Thiemann

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

    29 Citaten (Scopus)


    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. Keywords: automated termination analysis; cut; definite logic programs.
    Originele taal-2Engels
    Pagina's (van-tot)365-381
    TijdschriftTheory and Practice of Logic Programming
    Nummer van het tijdschrift4-6
    StatusGepubliceerd - 2010


    Duik in de onderzoeksthema's van 'Automated termination analysis for logic programs with cut'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit