\(\text{FO}=\text{FO}^3\) for linear orders with monotone binary relations. (English) Zbl 07561609
Baier, Christel (ed.) et al., 46th international colloquium on automata, languages, and programming, ICALP 2019, Patras, Greece, July 9–12, 2019. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 132, Article 116, 13 p. (2019).
Summary: 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 \((\mathbb{R},<,+1)\), and answers some open questions mentioned in a paper from T. Antonopoulos et al. [Lect. Notes Comput. Sci. 9034, 361–374 (2015; Zbl 1461.03020)]. 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.
For the entire collection see [Zbl 1414.68003].
For the entire collection see [Zbl 1414.68003].
Citations:
Zbl 1461.03020References:
| [1] | Timos Antonopoulos, Paul Hunter, Shahab Raza, and James Worrell. Three Variables Suffice for Real-Time Logic. In FoSSaCS 2015, volume 9034 of LNCS, pages 361-374. Springer, 2015. · Zbl 1461.03020 |
| [2] | Benedikt Bollig, Marie Fortin, and Paul Gastin. It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with “Happened Before”. In CONCUR 2018, volume 118 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2018. · Zbl 1487.68163 |
| [3] | Ryszard Danecki. Nondeterministic Propositional Dynamic Logic with intersection is decidable. In Computation Theory, pages 34-53. Springer Berlin Heidelberg, 1985. · Zbl 0608.03007 |
| [4] | Anuj Dawar. How Many First-order Variables are Needed on Finite Ordered Structures? In We Will Show Them! (1), pages 489-520. College Publications, 2005. · Zbl 1268.03037 |
| [5] | G. De Giacomo and M. Lenzerini. Boosting the Correspondence between Description Logics and Propositional Dynamic Logics. In Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31 -August 4, 1994, Volume 1., pages 205-212. AAAI Press / The MIT Press, 1994. |
| [6] | M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. · Zbl 0408.03014 |
| [7] | D. M. Gabbay. Expressive Functional Completeness in Tense Logic. In Uwe Mönnich, editor, Aspects of Philosophical Logic: Some Logical Forays into Central Notions of Linguistics and Philosophy, pages 91-117. Springer Netherlands, Dordrecht, 1981. · Zbl 0523.03017 |
| [8] | D. M. Gabbay, I. M. Hodkinson, and M. A. Reynolds. Temporal expressive completeness in the presence of gaps, volume Volume 2 of Lecture Notes in Logic, pages 89-121. Springer-Verlag, 1993. · Zbl 0802.03016 |
| [9] | S. Göller, M. Lohrey, and C. Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. Journal of Symbolic Logic, 74(1):279-314, 2009. · Zbl 1181.03034 |
| [10] | Martin Grohe. Finite variable logics in descriptive complexity theory. Bulletin of Symbolic Logic, 4(4):345-398, 1998. · Zbl 0940.03040 |
| [11] | J. Y. Halpern and Y. Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. Artif. Intell., 54(2):319-379, 1992. · Zbl 0762.68029 |
| [12] | L. Henkin. Logical Systems Containing Only a Finite Number of Symbols. Séminaire de Mathématiques Supérieures: Publications. Presses de l’Université de Montréal, 1967. · Zbl 0164.30702 |
| [13] | Yoram Hirshfeld and Alexander Rabinovich. Expressiveness of Metric modalities for continuous time. Logical Methods in Computer Science, 3(1), 2007. · Zbl 1128.03007 |
| [14] | Ian M. Hodkinson. Finite H-dimension does not imply expressive completeness. J. Philosophical Logic, 23(5):535-573, 1994. · Zbl 0811.03027 |
| [15] | Ian M. Hodkinson and András Simon. The k-variable property is stronger than H-dimension k. J. Philosophical Logic, 26(1):81-101, 1997. · Zbl 0976.03017 |
| [16] | Paul Hunter, Joël Ouaknine, and James Worrell. Expressive Completeness for Metric Temporal Logic. In LICS, pages 349-357. IEEE Computer Society, 2013. · Zbl 1366.03184 |
| [17] | Neil Immerman. Upper and Lower Bounds for First Order Expressibility. J. Comput. Syst. Sci., 25(1):76-98, 1982. · Zbl 0503.68032 |
| [18] | Neil Immerman. DSPACE[n k ] = VAR[k+1]. |
| [19] | In Structure in Complexity Theory Conference, pages 334-340. IEEE Computer Society, 1991. |
| [20] | Neil Immerman and Dexter Kozen. Definability with Bounded Number of Bound Variables. Inf. Comput., 83(2):121-139, 1989. · Zbl 0711.03004 |
| [21] | H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. |
| [22] | Michal Koucký, Clemens Lautemann, Sebastian Poloczek, and Denis Thérien. Circuit Lower Bounds via Ehrenfeucht-Fraisse Games. In IEEE Conference on Computational Complexity, pages 190-201. IEEE Computer Society, 2006. |
| [23] | M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39-49, 2006. · Zbl 1095.68053 |
| [24] | M. Lange and C. Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 70(5):1072-1086, 2005. · Zbl 1100.03017 |
| [25] | Carsten Lutz and Dirk Walther. PDL with negation of atomic programs. Journal of Applied Non-Classical Logics, 15(2):189-213, 2005. · Zbl 1185.03058 |
| [26] | Bruno Poizat. Deux Ou Trois Choses Que Je Sais de Ln. Journal of Symbolic Logic, 47(3):641-658, 1982. · Zbl 0507.03014 |
| [27] | Benjamin Rossman. On the constant-depth complexity of k-clique. In Proceedings of the 40th Annual ACM Symposium on Theory of Computing, Victoria, British Columbia, Canada, May 17-20, 2008, pages 721-730. ACM, 2008. · Zbl 1231.68154 |
| [28] | R. S. Streett. Propositional Dynamic Logic of Looping and Converse. In Proceedings of STOC’81, pages 375-383. ACM, 1981. |
| [29] | Alfred Tarski and Steven R. Givant. A formalization of set theory without variables. American Mathematical Society Providence, R.I, 1987. · Zbl 0654.03036 |
| [30] | Yde Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. · Zbl 0725.03006 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
