Loop detection in term rewriting using the eliminating unfoldings

DOI10.1016/j.tcs.2008.05.013zbMath1154.68436MaRDI QIDQ944383

Étienne Payet

Publication date: 16 September 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.univ-reunion.fr/hal-01186183/file/Loop_detection_in_term_rewriting_using_eliminating_unfoldings.pdf

zbMATH Keywords

loop; unfoldings; term rewriting system; non-termination; useless rule

Mathematics Subject Classification ID

68Q42: Grammars and rewriting systems

Related Items

Loop detection by logically constrained term rewriting, Lower bounds for runtime complexity of term rewriting, A non-termination criterion for binary constraint logic programs, Loops under Strategies

Uses Software

• MiniSat
• Tyrolean
• AProVE
• Matchbox

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rewriting techniques and applications. 15th international conference, RTA 2004, Aachen, Germany, June 3--5, 2004. Proceedings.
• Semi-unification
• Termination of string rewriting proved automatically
• A calculus of logical relations for over- and underapproximating static analyses
• Tyrolean termination tool: techniques and features
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Match-bounded string rewriting systems
• Foundations of equational logic programming
• Rules + strategies for transforming lazy functional logic programs
• Termination of term rewriting using dependency pairs
• A lattice-theoretical fixpoint theorem and its applications
• Inferring Termination Conditions for Logic Programs Using Backwards Analysis
• On Proving Uniform Termination and Restricted Termination of Rewriting Systems
• Abstract Diagnosis of Functional Programs
• Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator
• Grammar Analysis and Parsing by Abstract Interpretation
• A Transformation System for Developing Recursive Programs
• The integration of functions into logic programming: From theory to practice
• Analyses of unsatisfiability for equational logic programming
• cTI: a constraint-based termination inference tool for ISO-Prolog
• Term Rewriting and All That
• Non-Looping String Rewriting
• A semantic basis for the termination analysis of logic programs
• Narrowing directed by a graph of terms
• Theory and Applications of Satisfiability Testing
• Static Analysis
• Frontiers of Combining Systems
• Logic for Programming, Artificial Intelligence, and Reasoning