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.
@InProceedings{krebs_et_al:LIPIcs.CSL.2018.28, author = {Krebs, Andreas and Lodaya, Kamal and Pandya, Paritosh K. and Straubing, Howard}, title = {{An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {28:1--28:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.28}, URN = {urn:nbn:de:0030-drops-96953}, doi = {10.4230/LIPIcs.CSL.2018.28}, annote = {Keywords: two-variable logic, finite model theory, algebraic automata theory} }
Feedback for Dagstuhl Publishing