Finding Regular Herbrand Models for CHCs using Answer Set Programming

Gregoire Maire, Thomas Genet

We are interested in proving satisfiability of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). We propose to prove satisfiability by building a tree automaton rec…