Satisfying KBO Constraints

TL;DR

This paper introduces two novel methods for efficiently proving termination of rewrite systems using the Knuth-Bendix order by encoding constraints into propositional logic and testing for satisfiability.

Contribution

It presents new approaches that encode weight and precedence constraints into propositional logic, enabling efficient termination proofs for rewrite systems.

Findings

Encoding constraints into propositional logic is effective for termination proofs.

The methods can determine suitable weight functions and precedences automatically.

The approaches improve efficiency over previous techniques.

Abstract

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.