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

TL;DR

Initial Limit Datalog is a new, extensible class of constrained Horn clauses with decidable satisfiability, generalizing limit Datalog$_Z$ to higher-order logic and various background theories, enabling effective model checking.

Contribution

The paper introduces initial limit Datalog, expanding the class of decidable constrained Horn clauses to higher-order logic with background theories, and develops entwined structures for satisfiability witnessing.

Findings

Decidability of satisfiability over various background theories

Existence of recursively enumerable entwined structures

Model checking is decidable for initial limit Datalog

Abstract

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.