scholarly journals A General Framework for Automatic Termination Analysis of Logic Programs

2001 ◽  
Vol 12 (1-2) ◽  
pp. 117-156 ◽  
Author(s):  
Nachum Dershowitz ◽  
Naomi Lindenstrauss ◽  
Yehoshua Sagiv ◽  
Alexander Serebrenik
Keyword(s):  
General Framework ◽  
Logic Programs ◽  
Termination Analysis

scholarly journals Reuse of Results in Termination Analysis of Typed Logic Programs

2002 ◽  
pp. 477-492 ◽  
Author(s):  
Maurice Bruynooghe ◽  
Michael Codish ◽  
Samir Genaim ◽  
Wim Vanhoof
Keyword(s):  
Logic Programs ◽  
Termination Analysis

scholarly journals Termination analysis of logic programs through combination of type-based norms

2007 ◽  
Vol 29 (2) ◽  
pp. 10 ◽  
Author(s):  
Maurice Bruynooghe ◽  
Michael Codish ◽  
John P. Gallagher ◽  
Samir Genaim ◽  
Wim Vanhoof
Keyword(s):  
Logic Programs ◽  
Termination Analysis

scholarly journals Polytool: Polynomial interpretations as a basis for termination analysis of logic programs

2010 ◽  
Vol 11 (1) ◽  
pp. 33-63 ◽  
Author(s):  
MANH THANG NGUYEN ◽  
DANNY DE SCHREYE ◽  
JÜRGEN GIESL ◽  
PETER SCHNEIDER-KAMP
Keyword(s):  
Logic Programs ◽  
Termination Analysis ◽  
Rewrite Systems ◽  
Analysis Techniques ◽  
Programming Paradigm ◽  
Generating Polynomial ◽  
Direct Generalization ◽  
Term Rewrite Systems

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.

scholarly journals A General Framework for Static Cost Analysis of Parallel Logic Programs

2020 ◽  
pp. 19-35
Author(s):  
Maximiliano Klemen ◽  
Pedro López-García ◽  
John P. Gallagher ◽  
José F. Morales ◽  
Manuel V. Hermenegildo
Keyword(s):  
Cost Analysis ◽  
General Framework ◽  
Logic Programs

scholarly journals Automated termination analysis for logic programs with cut

2010 ◽  
Vol 10 (4-6) ◽  
pp. 365-381 ◽  
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.

Sign in / Sign up

Export Citation Format

Share Document