Automated termination proofs for logic programs by term rewriting
From MaRDI portal
Publication:2946588
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
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