Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling

ABSTRACT. We SAT-encode constraints for termination orders based on semantic labelling, argument filters, and recursive path orders, within the dependency pairs framework.

We specify constraints in a high-level Haskell-like language, and translate to SAT fully automatically by the CO4 compiler. That way, constraints can be combined easily.

This allows to write a single constraint for: find a model, and a sequence of ordering constraints for the labelled system, such that at least one original rule can be removed completely.

As an application, we produce a termination proof, verified by CeTA, for TRS/Aprove/JFP\_Ex31.