eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-07-04
116:1
116:13
10.4230/LIPIcs.ICALP.2019.116
article
FO = FO^3 for Linear Orders with Monotone Binary Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)
Fortin, Marie
1
LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, France
We show that over the class of linear orders with additional binary relations satisfying some monotonicity conditions, monadic first-order logic has the three-variable property. This generalizes (and gives a new proof of) several known results, including the fact that monadic first-order logic has the three-variable property over linear orders, as well as over (R,<,+1), and answers some open questions mentioned in a paper from Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on a translation of monadic first-order logic formulas into formulas of a star-free variant of Propositional Dynamic Logic, which are in turn easily expressible in monadic first-order logic with three variables.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol132-icalp2019/LIPIcs.ICALP.2019.116/LIPIcs.ICALP.2019.116.pdf
first-order logic
three-variable property
propositional dynamic logic