将LREC与LFP分离
Separating LREC from LFP
摘要：
LREC=是一阶逻辑的扩展，带有对数递归运算符。它是由Grohe等人提出的，并被证明可以捕获树和区间图上的复杂性类L。它一般不捕获L，因为它包含在FPC中-具有计数的定点逻辑。我们表明，这种遏制是严格的。特别是，我们表明，路径系统的问题，一个经典的P-完全问题，这是在LFP定义-不动点逻辑-是不可定义的LREC=这表明，对数递归机制是可证明的弱于一般的最小不动点。这个证明是基于一个为这个逻辑量身定制的新颖的破坏者复制者游戏。
英文摘要：
LREC= is an extension of first-order logic with a logarithmic recursion operator. It was introduced by Grohe et al. and shown to capture the complexity class L over trees and interval graphs. It does not capture L in general as it is contained in FPC - fixed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic P-complete problem which is definable in LFP - fixed-point logic - is not definable in LREC= This shows that the logarithmic recursion mechanism is provably weaker than general least fixed points. The proof is based on a novel Spoiler-Duplicator game tailored for this logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
