Compiling Existential Positive Queries to Bounded-Variable Fragments
Compiling Existential Positive Queries to Bounded-Variable Fragments
复制标题
将存在正查询编译为有界变量片段
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Hubie Chen
中科院分区：
文献类型：
--
作者：
Christoph Berkholz;Hubie Chen
一阶逻辑的有界变量片段的一个重要性质是它们可以在多项式时间内求值。因此，如果可能的话，将一阶查询重写为具有最少变量数量的逻辑等价查询，这是一个有用的预处理步骤。然而，减少变量的数量可能会导致公式大小的增加。我们研究了一阶查询的存在正片断的这种权衡，其中变量最小化通常是可决定的。特别地，我们研究了当编译对正一阶逻辑的有界变量片段的存在-正查询时公式大小的爆破。虽然公式大小的增长总是至多是指数级的，但我们确定了只需要多项式爆破的情况(基于签名和变量数量)。在所有其他情况下，我们证明了与一般上限匹配的编译公式的公式大小的指数下界。这个指数下限是无条件的，并且是关于所研究的编译的公式大小的第一个无条件下限；它通过建立一个新的与电路复杂性的接口得到了证明，这可能是未来感兴趣的。
A crucial property of bounded-variable fragments of first-order logic is that they can be evaluated in polynomial time. It is therefore a useful preprocessing step to rewrite, if possible, a first-order query to a logically equivalent one with a minimum number of variables. However, it may occur that reducing the number of variables causes an increase in formula size. We investigate this trade-off for the existential-positive fragment of first-order queries, where variable minimisation is decidable in general. In particular, we study the blow-up in the formula size when compiling existential-positive queries to the bounded variable fragment of positive first-order logic. While the increase of the formula size is always at most exponential, we identify situations (based on the signature and the number of variables) where only a polynomial blow-up is needed. In all other cases, we show that an exponential lower bound on the formula size of the compiled formula that matches the general upper bound. This exponential lower bound is unconditional, and is the first unconditional lower bound for formula size with respect to the studied compilation; it is proved via establishing a novel interface with circuit complexity which may be of future interest.
影响因子：
14.4
作者：
Gottlob, Georg;Kikot, Stanislav;Zakharyaschev, Michael
通讯作者：
Zakharyaschev, Michael
深度有界结构上的阶不变逻辑的简洁性
DOI：
10.1145/3152770
发表时间：
2017
期刊：
ACM Transactions on Computational Logic (TOCL)
影响因子：
--
作者：
K. Eickmeyer;M. Elberfeld;F. Harwath
通讯作者：
F. Harwath