Effective interpolation and preservation in guarded logics
Effective interpolation and preservation in guarded logics
复制标题
受保护逻辑中的有效插值和保存
DOI：
10.1145/2603088.2603108
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. V. Boom
中科院分区：
文献类型：
--
作者：
Michael Benedikt;B. T. Cate;M. V. Boom
逻辑的理想特性包括可决定性，以及继承一阶逻辑属性的模型理论，例如插值和保存定理。众所周知，一阶逻辑的保护片段（GF）是可以决定的，并且满足了一阶模型理论的一些保存特性。但是，它没有Craig插值。众所周知，刚定义的延伸片（GNF）是可决定的，并且具有Craig插值。在这里，我们给出了有关GF扩展的有效插值的第一个结果。我们为GNF提供了一个插值程序，其复杂性与GNF满足的双重指数上限相匹配。我们表明，相同的结构不仅提供了Craig插值，还提供了Lyndon的插值和相对插值，可用于提供一些保存定理的有效证明。我们为GNF和GF输入的GNF插值剂的尺寸提供上限，并与匹配的下限进行补充。
Desirable properties of a logic include decidability, and a model theory that inherits properties of first-order logic, such as interpolation and preservation theorems. It is known that the Guarded Fragment (GF) of first-order logic is decidable and satisfies some preservation properties from first-order model theory; however, it fails to have Craig interpolation. The Guarded Negation Fragment (GNF), a recently-defined extension, is known to be decidable and to have Craig interpolation. Here we give the first results on effective interpolation for extensions of GF. We provide an interpolation procedure for GNF whose complexity matches the doubly exponential upper bound for satisfiability of GNF. We show that the same construction gives not only Craig interpolation, but Lyndon interpolation and Relativized interpolation, which can be used to provide effective proofs of some preservation theorems. We provide upper bounds on the size of GNF interpolants for both GNF and GF input, and complement this with matching lower bounds.