Demand-driven and constraint-based automatic left-termination analysis for Logic Programs

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

Download Full-text

A General Framework for Automatic Termination Analysis of Logic Programs

Applicable Algebra in Engineering Communication and Computing ◽

10.1007/s002000100065 ◽

2001 ◽

Vol 12 (1-2) ◽

pp. 117-156 ◽

Cited By ~ 43

Author(s):

Nachum Dershowitz ◽

Naomi Lindenstrauss ◽

Yehoshua Sagiv ◽

Alexander Serebrenik

Keyword(s):

General Framework ◽

Logic Programs ◽

Termination Analysis

Download Full-text

Non-termination Analysis of Logic Programs Using Types

Logic-Based Program Synthesis and Transformation - Lecture Notes in Computer Science ◽

10.1007/978-3-642-20551-4_9 ◽

2011 ◽

pp. 133-148 ◽

Cited By ~ 2

Author(s):

Dean Voets ◽

Danny De Schreye

Keyword(s):

Logic Programs ◽

Termination Analysis

Download Full-text

Automatic Termination Analysis of Logic Programs

Logic Programming ◽

10.7551/mitpress/4299.003.0011 ◽

1997 ◽

Keyword(s):

Logic Programs ◽

Termination Analysis

Download Full-text

Automated termination analysis for logic programs with cut

Theory and Practice of Logic Programming ◽

10.1017/s1471068410000165 ◽

2010 ◽

Vol 10 (4-6) ◽

pp. 365-381 ◽

Cited By ~ 15

Author(s):

PETER SCHNEIDER-KAMP ◽

JÜRGEN GIESL ◽

THOMAS STRÖDER ◽

ALEXANDER SEREBRENIK ◽

RENÉ THIEMANN

Keyword(s):

Real World ◽

Processing Method ◽

Logic Programs ◽

Termination Analysis ◽

Original Program ◽

Almost All

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

Download Full-text

On termination of meta-programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068404002248 ◽

2005 ◽

Vol 5 (3) ◽

pp. 355-390 ◽

Cited By ~ 8

Author(s):

ALEXANDER SEREBRENIK ◽

DANNY DE SCHREYE

Keyword(s):

Broad Class ◽

The Other ◽

Writing Programs ◽

Logic Programs ◽

Termination Analysis ◽

Rewrite Systems ◽

Term Rewrite Systems ◽

Meta Programming

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

Download Full-text