Predictive Labeling with Dependency Pairs Using SAT

DOI10.1007/978-3-540-73595-3_31zbMath1213.68349OpenAlexW2147996890MaRDI QIDQ3608786

Aart Middeldorp, Adam Koprowski

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_31

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

KBO orientability, SAT solving for termination proofs with recursive path orders and dependency pairs, Root-Labeling, Transforming SAT into Termination of Rewriting, Innermost Termination of Rewrite Systems by Labeling

Uses Software

• MiniSat
• Tyrolean