Automated Termination Analysis for Logic Programs with Cut

Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TidsskriftTheory and Practice of Logic Programming
Vol/bind10
Udgave nummer4-6
Sider (fra-til)365
Antal sider381
ISSN1471-0684
DOI
StatusUdgivet - 2010

Fingeraftryk

Logic Programs
Termination
Processing
Preprocessing
Prolog
Experiments
Transform
Imply
Operator
Experiment

Citer dette

Schneider-Kamp, Peter ; Giesl, Jürgen ; Ströder, Thomas ; Serebrenik, Alexander ; Thiemann, René. / Automated Termination Analysis for Logic Programs with Cut. I: Theory and Practice of Logic Programming. 2010 ; Bind 10, Nr. 4-6. s. 365.
@article{f4cbd8352db34dd8b053200d6a0cbec9,
title = "Automated Termination Analysis for Logic Programs with Cut",
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.",
author = "Peter Schneider-Kamp and J{\"u}rgen Giesl and Thomas Str{\"o}der and Alexander Serebrenik and Ren{\'e} Thiemann",
year = "2010",
doi = "10.1017/S1471068410000165",
language = "English",
volume = "10",
pages = "365",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Heinemann",
number = "4-6",

}

Automated Termination Analysis for Logic Programs with Cut. / Schneider-Kamp, Peter; Giesl, Jürgen; Ströder, Thomas; Serebrenik, Alexander; Thiemann, René.

I: Theory and Practice of Logic Programming, Bind 10, Nr. 4-6, 2010, s. 365.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Automated Termination Analysis for Logic Programs with Cut

AU - Schneider-Kamp, Peter

AU - Giesl, Jürgen

AU - Ströder, Thomas

AU - Serebrenik, Alexander

AU - Thiemann, René

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1017/S1471068410000165

DO - 10.1017/S1471068410000165

M3 - Journal article

VL - 10

SP - 365

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 4-6

ER -