Automated termination analysis for logic programs with cut

DOI10.1017/S1471068410000165MaRDI QIDQ3585154zbMATHOpenAlexFDO

Authors Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann

Publication date 19 August 2010

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.4908

zbMATH Keywords

cutdefinite logic programsautomated termination analysis

Mathematics Subject Classification ID

Logic programming (68N17)

Abstract: Termination 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.

Recommendations

• Automated Termination Analysis for Logic Programs by Term Rewriting
• A general framework for automatic termination analysis od logic programs
• Automated termination proofs for logic programs by term rewriting
• Dependency triples for improving termination analysis of logic programs with cut
• A semantic basis for the termination analysis of logic programs
• scientific article; zbMATH DE number 1834571
• A methodology for proving termination of logic programs
• Termination Analysis of Logic Programs Based on Dependency Graphs

Cited in

(10)

• Automated Termination Analysis for Logic Programs by Term Rewriting
• A framework for computing finite SLD trees
• Checking termination of bottom-up evaluation of logic programs with function symbols
• A dependency pair framework for innermost complexity analysis of term rewrite systems
• Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
• Dependency triples for improving termination analysis of logic programs with cut
• A practical analysis of non-termination in large logic programs
• Automated termination proofs for logic programs by term rewriting
• Using linear constraints for logic program termination analysis
• Proving completeness of logic programs with the cut

This page was built for publication: Automated termination analysis for logic programs with cut

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585154)