{"ID":2848021,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.26428","arxiv_id":"2510.26428","title":"Finding Regular Herbrand Models for CHCs using Answer Set Programming","abstract":"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 recognizing the Herbrand model of the CHCs. If such an automaton exists then the model is said to be regular, i.e., the Herbrand model is a regular set of atoms. Kostyukov et al. have shown how to derive an automaton when CVC4 finds a finite model of the CHCs. We propose an alternative way to build the automaton using an encoding into a SAT problem using Clingo, an Answer Set Programming (ASP) tool. We implemented a translation of CHCs with ADTs into an ASP problem. Combined with Clingo, we obtain a semi-complete satisfiability checker: it finds a tree automaton if a regular Herbrand model exists or finds a counter-example if the problem is unsatisfiable.","short_abstract":"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 recognizing the Herbrand model of the CHCs. If such an automaton exists then the model is said to be regular, i.e., the Herbrand model is a reg...","url_abs":"https://arxiv.org/abs/2510.26428","url_pdf":"https://arxiv.org/pdf/2510.26428v1","authors":"[\"Gregoire Maire\",\"Thomas Genet\"]","published":"2025-10-30T12:24:23Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.FL\",\"cs.PL\"]","methods":"[]","has_code":false}