Automated termination analysis for logic programs with cut

DOI10.1017/S1471068410000165zbMATH Open1209.68098arXiv1007.4908OpenAlexW2128219525MaRDI QIDQ3585154FDOQ3585154

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)

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.

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

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

zbMATH Keywords

cutdefinite logic programsautomated termination analysis

Mathematics Subject Classification ID

Logic programming (68N17)

Cited In (9)

• A framework for computing finite SLD trees
• 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
• Checking termination of bottom-up evaluation of logic programs with function symbols
• A dependency pair framework for innermost complexity analysis of term rewrite systems
• Using linear constraints for logic program termination analysis
• A practical analysis of non-termination in large logic programs
• Proving completeness of logic programs with the cut
• Automated Termination Analysis for Logic Programs by Term Rewriting

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)