Satisfying KBO Constraints
| dc.creator | Zankl, Harald | |
| dc.creator | Middeldorp, Aart | |
| dc.date | 2006-08-06 | |
| dc.date | 2007-04-03 | |
| dc.date.accessioned | 2026-07-07T07:54:48Z | |
| dc.date.available | 2026-07-07T07:54:48Z | |
| dc.description | This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in (pseudo-)propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such that the induced Knuth-Bendix order orients the rules of the encoded rewrite system from left to right. | |
| dc.description | 15 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0608032 | |
| dc.identifier | http://arxiv.org/abs/cs/0608032 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/126749 | |
| dc.subject | Symbolic Computation | |
| dc.subject | Logic in Computer Science | |
| dc.title | Satisfying KBO Constraints | |
| dc.type | text |