# Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses

arXiv: https://arxiv.org/abs/2104.14175 · HTML: https://mlsanity.com/paper/2104.14175/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Apr 2021.

## Built on by (most cited first, 1 of 1)

- [Complexity of Arithmetic in Warded Datalog+-](https://mlsanity.com/paper/2202.05086/) (2022)

## Abstract (arXiv)

We present initial limit Datalog, a new extensible class of constrained Horn clauses for which the satisfiability problem is decidable. The class may be viewed as a generalisation to higher-order logic (with a simple restriction on types) of the first-order language limit DatalogZ (a fragment of Datalog modulo linear integer arithmetic), but can be instantiated with any suitable background theory. For example, the fragment is decidable over any countable well-quasi-order with a decidable first-order theory, such as natural number vectors under componentwise linear arithmetic, and words of a bounded, context-free language ordered by the subword relation. Formulas of initial limit Datalog have the property that, under some assumptions on the background theory, their satisfiability can be witnessed by a new kind of term model which we call entwined structures. Whilst the set of all models is typically uncountable, the set of all entwined structures is recursively enumerable, and model checking is decidable.