文章基本信息

标题：An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation
本地全文：下载
作者：Andreas Krebs ; Kamal Lodaya ; Paritosh K. Pandya 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：119
页码：1-17
DOI：10.4230/LIPIcs.CSL.2018.28
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.
关键词：two-variable logic; finite model theory; algebraic automata theory