Propositional Encoding of Constraints over Tree-Shaped Data

2013/05/21 by Alexander Bau, Bau, Alexander, Johannes Waldmann +1
Computer Science · #FOS: Computer and information sciences #Programming Languages (cs.PL) #cs.PL

paper · pdf · doi:10.48550/arxiv.1305.4957

arxiv created 2013/05/21 · arxiv updated 2013/05/24

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.

Related

• Representing Constraints with Automata
• Parsing and Generation with Tabulation and Compilation
• Memoization of Coroutined Constraints
• Memoization in Constraint Logic Programming
• Constraint Logic Programming for Natural Language Processing