Propositional Encoding of Constraints over Tree-Shaped Data
Programming Languages
2013-05-24 v1
Abstract
We present a functional programming language for specifying constraints over tree-shaped data. The language allows for Haskell-like algebraic data types and pattern matching. Our constraint compiler CO4 translates these programs into satisfiability problems in propositional logic. We present an application from the area of automated analysis of (non-)termination of rewrite systems.
Keywords
Cite
@article{arxiv.1305.4957,
title = {Propositional Encoding of Constraints over Tree-Shaped Data},
author = {Alexander Bau and Johannes Waldmann},
journal= {arXiv preprint arXiv:1305.4957},
year = {2013}
}