Automated termination proofs for logic programs by term rewriting

DOI10.1145/1614431.1614433zbMath1351.68054arXiv0803.0014OpenAlexW2137327104MaRDI QIDQ2946588

Peter Schneider-Kamp, Alexander Serebrenik, René Thiemann, Jürgen Giesl

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

logic programmingterm rewritingdependency pairstermination analysis

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic programming (68N17)

Related Items (13)

Correctness and Completeness of Logic Programs ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ Terminating Evaluation of Logic Programs with Finite Three-Valued Models ⋮ Checking termination of bottom-up evaluation of logic programs with function symbols ⋮ Using linear constraints for logic program termination analysis ⋮ Conversion to tail recursion in term rewriting ⋮ Dependency Triples for Improving Termination Analysis of Logic Programs with Cut ⋮ Determinization of inverted grammar programs via context-free expressions ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Termination Graphs for Java Bytecode ⋮ A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs ⋮ Proving Termination of Integer Term Rewriting ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

This page was built for publication: Automated termination proofs for logic programs by term rewriting