Transforming SAT into Termination of Rewriting

DOI10.1016/j.entcs.2009.07.023zbMath1347.68202OpenAlexW2058475217MaRDI QIDQ4982632

Harald Zankl, Christian Sternagel, Aart Middeldorp

Publication date: 9 April 2015

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

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.717.5016

zbMATH Keywords

terminationterm rewritingSAT solvingsemantic labeling

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (1)

Termination of Cycle Rewriting by Transformation and Matrix Interpretation

Uses Software

• AProVE
• TPA
• Matchbox

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Automating the Knuth Bendix ordering
• Matrix interpretations for proving termination of term rewriting
• Termination of term rewriting: Interpretation and type elimination
• Orienting rewrite rules with the Knuth-Bendix order.
• Termination of term rewriting using dependency pairs
• Solving Partial Order Constraints for LPO Termination
• TPA: Termination Proved Automatically
• Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator
• Predictive Labeling with Dependency Pairs Using SAT
• Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
• Satisfying KBO Constraints
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Transforming SAT into Termination of Rewriting