We propose FC, a new logic on words that combines finite model theory with the theory of concatenation - a first-order logic that is based on word equations. Like the theory of concatenation, FC is built around word equations; in contrast to it, its semantics are defined to only allow finite models, by limiting the universe to a word and all its factors. As a consequence of this, FC has many of the desirable properties of FO on finite models, while being far more expressive than FO[<]. Most noteworthy among these desirable properties are sufficient criteria for efficient model checking, and capturing various complexity classes by adding operators for transitive closures or fixed points. Not only does FC allow us to obtain new insights and techniques for expressive power and efficient evaluation of document spanners, but it also provides a general framework for logic on words that also has potential applications in other areas.
翻译:我们提出了将有限模型理论与连接理论相结合的词句的新逻辑FC, 这是一种将有限模型理论与连接理论相结合的新的逻辑,一种基于单词方程的一阶逻辑。 与组合理论一样, FC是围绕单词方程建立的; 与之相反, 其语义定义仅允许有限模型, 将宇宙限制在一个单词和所有因素上。 因此, FC有许多FO在有限模型上的可取属性, 其表达性远大于FO[ 。 其中最值得注意的特性是高效模式检查的充足标准, 并通过增加中转封闭或固定点操作员来捕捉各种复杂类别。 FC不仅允许我们获得新的洞察力和技术, 以及表达力和有效评估文件横跨器的高效评估, 而且还为在其他领域也有潜在应用的词提供了逻辑框架。