TY - GEN
T1 - Automated termination analysis for logic programs by term rewriting
AU - Schneider-Kamp, P.
AU - Giesl, J.
AU - Serebrenik, A.
AU - Thiemann, R.
PY - 2007
Y1 - 2007
N2 - There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this paper we improve these transformations such that they become applicable for any definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.
AB - There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this paper we improve these transformations such that they become applicable for any definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.
U2 - 10.1007/978-3-540-71410-1_13
DO - 10.1007/978-3-540-71410-1_13
M3 - Conference contribution
SN - 978-3-540-71409-5
T3 - Lecture Notes in Computer Science
SP - 177
EP - 193
BT - Proceedings of the 16th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2006) 12-14 July 2006, Venice, Italy
A2 - Puebla, G.
PB - Springer
CY - Berlin
T2 - conference; LOPSTR 2006, Venice, Italy; 2007-07-12; 2007-07-14
Y2 - 12 July 2007 through 14 July 2007
ER -