AI 中文总结
本文研究超越二元元数的合并判定问题，针对语义 Horn 情形证明该问题可判定，其复杂度为 2EXPTIME，固定元数时为 EXPTIME，并给出基于局部一致性证书的判定程序。
AI 中文摘要
我们研究合并判定问题：给定一个全称一阶句子 Φ，判定其有限模型类 fm(Φ) 是否具有合并性质。若 fm(Φ) 在二元直积下封闭，则称 Φ 为语义 Horn。根据 McKinsey 定理，这等价于 Φ 逻辑等价于一个全称 Horn 句子；二者的区别仅在于输入表示，因为 Φ 本身无需以 Horn 形式给出，且转换为显式 Horn 范式可能会引发指数级膨胀。我们证明，在该语义约束下，此问题是可判定的。此外，该问题属于 2EXPTIME 复杂度类，且对于输入签名元数的每个固定界，它属于 EXPTIME 复杂度类。因此，语义 Horn 片段为具有无关节关系元数的签名提供了无条件的判定程序。我们的证明始于内外对应关系，将其作为语义归约到有限完备化问题的黑箱。我们将有限完备化编码为到有限关系模板的同态，并为模板具有有界宽度的完备化问题引入有限集值的局部一致性证书。对于语义 Horn 输入，每个固定源图上的局部完备化在添加关系的逐关系交下封闭，且这些交与限制映射兼容。这产生了完备化模板的半格多态性。由于模板是二元的，半格运算给出宽度为 2，使得局部一致性证书是完备的。只要关联的完备化模板具有有界宽度，相同的构造就会给出判定程序。
英文摘要
We study the amalgamation decision problem (ADP): given a universal first-order sentence $Φ$, decide whether the class $\mathrm{fm}(Φ)$ of its finite models has the amalgamation property. We call $Φ$ semantic Horn if $\mathrm{fm}(Φ)$ is closed under binary direct products. By McKinsey's theorem, this is equivalent to $Φ$ being logically equivalent to a universal Horn sentence. The distinction concerns the input representation: $Φ$ itself need not be given in Horn form, and converting it into an explicit Horn normal form can incur an exponential blow-up. We prove that the ADP is decidable under this semantic promise. To this end, we associate with $Φ$ a finite-domain CSP template, called its completion template, and a distinguished infinite family of CSP instances, called its atlas instances. The class $\mathrm{fm}(Φ)$ has the amalgamation property precisely when all atlas instances have a solution. For semantic Horn inputs, we prove that the completion template admits a semilattice polymorphism. Consequently, its CSP has bounded width and is decided by a fixed level of local consistency. We introduce uniform contextual strategies, finite certificates expressing this local-consistency condition simultaneously for all atlas instances, and give an effective fixed-point procedure for deciding whether such a certificate exists. The resulting algorithm runs in 2ExpTime in general and in ExpTime under any fixed bound on the arities of the input relations. More generally, the construction gives a decision procedure whenever the associated completion template has bounded width. These bounds are optimal: the semantic Horn ADP is 2ExpTime-complete in general and ExpTime-complete for every fixed arity bound of at least three. Both hardness results already hold for syntactic universal Horn sentences.
Comments47 pages, 6 figures
