Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs

J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, C. Fuhs

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. More information can be found in the full paper [1]. © 2013 Springer-Verlag.
OriginalsprogEngelsk
TitelLogic-Based Program Synthesis and Transformation
RedaktørerElvira Albert
Antal sider1
Vol/bind7844
ForlagSpringer
Publikationsdato2013
ISBN (Trykt)978-364238196-6
ISBN (Elektronisk)978-3-642-38197-3
DOI
StatusUdgivet - 2013
Begivenhed22nd International Symposium on Logic-Based Program Synthesis and Transformation - Leuven, Belgien
Varighed: 18. sep. 201220. sep. 2012

Konference

Konference22nd International Symposium on Logic-Based Program Synthesis and Transformation
LandBelgien
ByLeuven
Periode18/09/201220/09/2012
NavnLecture Notes in Computer Science
Vol/bind7844
ISSN0302-9743

Citer dette

Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., & Fuhs, C. (2013). Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs. I E. Albert (red.), Logic-Based Program Synthesis and Transformation (Bind 7844). Springer. Lecture Notes in Computer Science, Bind. 7844 https://doi.org/10.1007/978-3-642-38197-3_1
Giesl, J. ; Ströder, T. ; Schneider-Kamp, P. ; Emmes, F. ; Fuhs, C. / Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs. Logic-Based Program Synthesis and Transformation. red. / Elvira Albert. Bind 7844 Springer, 2013. (Lecture Notes in Computer Science, Bind 7844).
@inproceedings{c0e865e72fff4bbd978b6b5d3cca91b7,
title = "Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs",
abstract = "There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. More information can be found in the full paper [1]. {\circledC} 2013 Springer-Verlag.",
author = "J. Giesl and T. Str{\"o}der and P. Schneider-Kamp and F. Emmes and C. Fuhs",
year = "2013",
doi = "10.1007/978-3-642-38197-3_1",
language = "English",
isbn = "978-364238196-6",
volume = "7844",
editor = "Elvira Albert",
booktitle = "Logic-Based Program Synthesis and Transformation",
publisher = "Springer",
address = "Germany",

}

Giesl, J, Ströder, T, Schneider-Kamp, P, Emmes, F & Fuhs, C 2013, Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs. i E Albert (red.), Logic-Based Program Synthesis and Transformation. bind 7844, Springer, Lecture Notes in Computer Science, bind 7844, 22nd International Symposium on Logic-Based Program Synthesis and Transformation , Leuven, Belgien, 18/09/2012. https://doi.org/10.1007/978-3-642-38197-3_1

Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs. / Giesl, J.; Ströder, T.; Schneider-Kamp, P.; Emmes, F.; Fuhs, C.

Logic-Based Program Synthesis and Transformation. red. / Elvira Albert. Bind 7844 Springer, 2013. (Lecture Notes in Computer Science, Bind 7844).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs

AU - Giesl, J.

AU - Ströder, T.

AU - Schneider-Kamp, P.

AU - Emmes, F.

AU - Fuhs, C.

PY - 2013

Y1 - 2013

N2 - There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. More information can be found in the full paper [1]. © 2013 Springer-Verlag.

AB - There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. More information can be found in the full paper [1]. © 2013 Springer-Verlag.

U2 - 10.1007/978-3-642-38197-3_1

DO - 10.1007/978-3-642-38197-3_1

M3 - Article in proceedings

SN - 978-364238196-6

VL - 7844

BT - Logic-Based Program Synthesis and Transformation

A2 - Albert, Elvira

PB - Springer

ER -

Giesl J, Ströder T, Schneider-Kamp P, Emmes F, Fuhs C. Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs. I Albert E, red., Logic-Based Program Synthesis and Transformation. Bind 7844. Springer. 2013. (Lecture Notes in Computer Science, Bind 7844). https://doi.org/10.1007/978-3-642-38197-3_1