  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 Datalog$_Z$ (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.
