论文标题
在没有贝丝和克雷格的情况下生活：被保护和两变量的碎片中的定义和插值
Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments
论文作者
论文摘要
在具有Craig插值特性（CIP）的逻辑中，interpolant的存在是含义的含义。在带有Beth beth Distability属性（PBDP）的逻辑中，关系的明确定义的存在源于表达其隐式确定性的公式的有效性。一阶逻辑的两变量片段FO2和受保护的片段GF都无法具有CIP和PBDP。我们表明，在这两个片段中，插值的存在和明确的定义都是可决定的。在GF中，这两个问题通常都是3个问题，通常是2时组，如果关系符号的ARITY由不小于3的常数C界定。因此，对于GF和FO2的存在，插值的存在和显式定义都是可决定的，但比有效性更难（在标准复杂性假设下FO2的情况下）。
In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragment, GF, of first-order logic both fail to have the CIP and the PBDP. We show that nevertheless in both fragments the existence of interpolants and explicit definitions is decidable. In GF, both problems are 3ExpTime-complete in general, and 2ExpTime-complete if the arity of relation symbols is bounded by a constant c not smaller than 3. In FO2, we prove a coN2ExpTime upper bound and a 2ExpTime lower bound for both problems. Thus, both for GF and FO2 existence of interpolants and explicit definitions are decidable but harder than validity (in case of FO2 under standard complexity assumptions).
