Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs

Manh Thang Nguyen, Danny De Schreye, Jürgen Giesl, Peter Schneider-Kamp

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.
OriginalsprogEngelsk
TidsskriftTheory and Practice of Logic Programming
Vol/bind11
Sider (fra-til)33-63
ISSN1471-0684
DOI
StatusUdgivet - 2011

Fingeraftryk

Logic Programs
Termination
Polynomials
Polynomial
Paradigm
Interpretation
Programming
Norm
Generalise
Arbitrary
Term

Citer dette

@article{1b2d7e9e8e4f4a059a04bc9380a9e318,
title = "Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs",
abstract = "Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.",
author = "Nguyen, {Manh Thang} and {De Schreye}, Danny and J{\"u}rgen Giesl and Peter Schneider-Kamp",
year = "2011",
doi = "10.1017/S1471068410000025",
language = "English",
volume = "11",
pages = "33--63",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Heinemann",

}

Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs. / Nguyen, Manh Thang; De Schreye, Danny; Giesl, Jürgen; Schneider-Kamp, Peter.

I: Theory and Practice of Logic Programming, Bind 11, 2011, s. 33-63.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs

AU - Nguyen, Manh Thang

AU - De Schreye, Danny

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

PY - 2011

Y1 - 2011

N2 - Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

AB - Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

U2 - 10.1017/S1471068410000025

DO - 10.1017/S1471068410000025

M3 - Journal article

VL - 11

SP - 33

EP - 63

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

ER -