一句话：提出初始极限 Datalog，将可判定极限 DatalogZ 推广到高阶并支持任意合适背景理论。
本文研究约束霍恩子句的可判定性，提出初始极限 Datalog。该片段可视为一阶语言 limit DatalogZ（Datalog 模线性整数算术）在带简单类型限制的高阶逻辑上的推广，并可实例化到任意合适的背景理论。作者证明，在一类可判定一阶理论上，例如按分量线性算术的自然数向量以及按子词序排序的有界上下文无关语言词，其可满足性可判定。关键方法是构造一种新的项模型——纠缠结构（entwined structures），用来见证可满足性。虽然全体模型通常不可数，但所有纠缠结构递归可枚举，且模型检测可判定。
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.
@inproceedings{paperbot6222,
title = {Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses},
author = {Toby Cathcart Burn and Luke Ong and Steven Ramsay and Dominik Wagner},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470527}
}