Document Open Access Logo

FO = FO^3 for Linear Orders with Monotone Binary Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)

Author Marie Fortin

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2019.116.pdf
  • Filesize: 0.51 MB
  • 13 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • first-order logic
  • three-variable property
  • propositional dynamic logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Marie Fortin. FO = FO^3 for Linear Orders with Monotone Binary Relations (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 116:1-116:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.116

Author Details

Marie Fortin
  • LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, France

References

  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. Google Scholar
  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. Google Scholar
  3. Ryszard Danecki. Nondeterministic Propositional Dynamic Logic with intersection is decidable. In Computation Theory, pages 34-53. Springer Berlin Heidelberg, 1985. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  10. Martin Grohe. Finite variable logics in descriptive complexity theory. Bulletin of Symbolic Logic, 4(4):345-398, 1998. Google Scholar
  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. Google Scholar
  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. Google Scholar
  13. Yoram Hirshfeld and Alexander Rabinovich. Expressiveness of Metric modalities for continuous time. Logical Methods in Computer Science, 3(1), 2007. Google Scholar
  14. Ian M. Hodkinson. Finite H-dimension does not imply expressive completeness. J. Philosophical Logic, 23(5):535-573, 1994. Google Scholar
  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. Google Scholar
  16. Paul Hunter, Joël Ouaknine, and James Worrell. Expressive Completeness for Metric Temporal Logic. In LICS, pages 349-357. IEEE Computer Society, 2013. Google Scholar
  17. Neil Immerman. Upper and Lower Bounds for First Order Expressibility. J. Comput. Syst. Sci., 25(1):76-98, 1982. Google Scholar
  18. Neil Immerman. DSPACE[n^k] = VAR[k+1]. In Structure in Complexity Theory Conference, pages 334-340. IEEE Computer Society, 1991. Google Scholar
  19. Neil Immerman and Dexter Kozen. Definability with Bounded Number of Bound Variables. Inf. Comput., 83(2):121-139, 1989. Google Scholar
  20. H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. Google Scholar
  21. 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. Google Scholar
  22. M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39-49, 2006. Google Scholar
  23. M. Lange and C. Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 70(5):1072-1086, 2005. Google Scholar
  24. Carsten Lutz and Dirk Walther. PDL with negation of atomic programs. Journal of Applied Non-Classical Logics, 15(2):189-213, 2005. Google Scholar
  25. Bruno Poizat. Deux Ou Trois Choses Que Je Sais de Ln. Journal of Symbolic Logic, 47(3):641-658, 1982. Google Scholar
  26. 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. Google Scholar
  27. R. S. Streett. Propositional Dynamic Logic of Looping and Converse. In Proceedings of STOC'81, pages 375-383. ACM, 1981. Google Scholar
  28. Alfred Tarski and Steven R. Givant. A formalization of set theory without variables. American Mathematical Society Providence, R.I, 1987. Google Scholar
  29. Yde Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact