Abstract

We discuss design choices for SAT-encoding constraints for termination orders based on semantic labelling and unlabelling, linear interpretations, recursive path orders with argument filters, 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. Reliability is achieved via certification of generated proofs. The size of the resulting propositional logic formulas can be reduced by strengthening the constraints. We discuss an encoding of finite maps via patterns.

BibTeX

@inproceedings{ABRTJW-WST14,
  author    = "Alexander Bau and Ren{\'e} Thiemann and Johannes Waldmann",
  title     = "Automated {SAT} Encoding for Termination Proofs with
               Semantic Labelling and Unlabelling",
  booktitle = "Proceedings of the 14th International Workshop on
               Termination",
  editor    = "Carsten Fuhs",
  pages     = "6--10",
  year      = 2014
}