Document Open Access Logo

Binding Forms in First-Order Logic

Authors Fabio Mogavero, Giuseppe Perelli

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.648.pdf
  • Filesize: 0.62 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • First-Order Logic
  • Decidable Fragments
  • Satisfiability
  • Model Checking

Metrics

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

Abstract

Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.

Cite As Get BibTex

Fabio Mogavero and Giuseppe Perelli. Binding Forms in First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 648-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.648

Author Details

Fabio Mogavero
Giuseppe Perelli

References

  1. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. Google Scholar
  2. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-Time Temporal Logic. JACM, 49(5):672-713, 2002. Google Scholar
  3. H. Andréka, J. van Benthem, and I. Németi. Modal Languages And Bounded Fragments Of Predicate Logic. JPL, 27(3):217-274, 1998. Google Scholar
  4. V. Bárány, M. Benedikt, and B. ten Cate. Rewriting Guarded Negation Queries. In MFCS'13, LNCS 8087, pages 98-110. Springer, 2013. Google Scholar
  5. V. Bárány, G. Gottlob, and M. Otto. Querying the Guarded Fragment. In LICS'10, pages 1-10. IEEE Computer Society, 2010. Google Scholar
  6. V. Bárány, B. ten Cate, and M. Otto. Queries with Guarded Negation. PVLDB, 5(11):1328-1339, 2012. Google Scholar
  7. V. Bárány, B. ten Cate, and L. Segoufin. Guarded Negation. In ICALP'11, LNCS 6756, pages 356-367. Springer, 2011. Google Scholar
  8. M. Ben-Ari. Mathematical Logic for Computer Science (3rd ed.). Springer, 2012. Google Scholar
  9. D. Berwanger and E. Grädel. Games and Model Checking for Guarded Logics. In LPAR'01, LNCS 2250, pages 70-84. Springer, 2001. Google Scholar
  10. E. Börger. Decision Problems in Predicate Logic. In LC'82, volume 112, pages 263-301. Elsevier, 1984. Google Scholar
  11. E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997. Google Scholar
  12. K. Chatterjee, T.A. Henzinger, and N. Piterman. Strategy Logic. In CONCUR'07, LNCS 4703, pages 59-73. Springer, 2007. Google Scholar
  13. E.F. Codd. A Relational Model of Data for Large Shared Data Banks. CACM, 13(6):377-387, 1970. Google Scholar
  14. E.F. Codd. Relational Completeness of Data Base Sublanguages. DS, pages 65-98, 1972. Google Scholar
  15. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 1995. Google Scholar
  16. R. Fagin and M.Y. Vardi. The Theory of Data Dependencies - A Survey. MIP, 34:19-71, 1972. Google Scholar
  17. E. Fredkin. Trie Memory. CACM, 3(9):490-499, 1960. Google Scholar
  18. E. Goncalves and E. Grädel. Decidability Issues for Action Guarded Logics. In DL'00, pages 123-132, 2000. Google Scholar
  19. E. Grädel. Decision Procedures for Guarded Logics. In CADE'99, LNCS 1632, pages 31-51. Springer, 1999. Google Scholar
  20. E. Grädel. On The Restraining Power of Guards. JSL, 64(4):1719-1742, 1999. Google Scholar
  21. E. Grädel. Why are Modal Logics so Robustly Decidable? In CTTCS'01, pages 393-408. World Scientific, 2001. Google Scholar
  22. E. Grädel. Guarded Fixed Point Logics and the Monadic Theory of Countable Trees. TCS, 288(1):129-152, 2002. Google Scholar
  23. E. Grädel. Decidable Fragments of First-Order and Fixed-Point Logic. In KWLCS'03, 2003. Google Scholar
  24. E. Grädel, P.G. Kolaitis, and M.Y. Vardi. On the Decision Problem for Two-Variable First-Order Logic. BSL, 3(1):53-69, 1997. Google Scholar
  25. E. Grädel and I. Walukiewicz. Guarded Fixed Point Logic. In LICS'99, pages 45-54. IEEE Computer Society, 1999. Google Scholar
  26. Lauri Hella and A. Kuusisto. One-Dimensional Fragment of First-Order Logic. In AIML'14, pages 274-293. College Publications, 2014. Google Scholar
  27. D. Hilbert and W. Ackermann. Grundzüge der Theoretischen Logik. Die Grundlehren der Mathematischen Wissenschaften. Springer, 1928. Google Scholar
  28. I. Hodkinson. Loosely Guarded Fragment of First-Order Logic has the Finite Model Property. SL, 70(2):205-240, 2002. Google Scholar
  29. E. Hoogland and M. Marx. Interpolation and Definability in Guarded Fragments. SL, 70(3):373-409, 2002. Google Scholar
  30. N. Immerman. Number of Quantifiers is Better Than Number of Tape Cells. JCSS, 22(3):384-406, 1981. Google Scholar
  31. N. Immerman. Relational Queries Computable in Polynomial Time (Extended Abstract). In STOC'82, pages 147-152. Association for Computing Machinery, 1982. Google Scholar
  32. N. Immerman. Relational Queries Computable in Polynomial Time. IC, 68(1-3):86-104, 1986. Google Scholar
  33. N. Immerman. Descriptive Complexity. Springer, 1999. Google Scholar
  34. E. Kieronski and A. Kuusisto. Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality. In MFCS'14, LNCS 8634, pages 365-376. Springer, 2014. Google Scholar
  35. L. Löwenheim. Über Möglichkeiten im Relativkalkül. MA, 76(4):447-470, 1915. Google Scholar
  36. F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. Reasoning About Strategies: On the Satisfiability Problem. Under submission. Google Scholar
  37. F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. What Makes \ATLS Decidable? A Decidable Fragment of Strategy Logic. In CONCUR'12, LNCS 7454, pages 193-208. Springer, 2012. Google Scholar
  38. F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. TOCL, 15(4):34:1-42, 2014. Google Scholar
  39. F. Mogavero, A. Murano, and M.Y. Vardi. Reasoning About Strategies. In FSTTCS'10, LIPIcs 8, pages 133-144. Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  40. M. Mortimer. On Languages with Two Variables. MLQ, 21(1):135-140, 1975. Google Scholar
  41. A. Onet. The Chase Procedure and its Applications in Data Exchange. In Data Exchange, Integration, and Streams., pages 1-37. Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  42. W.C. Purdy. Complexity and Nicety of Fluted Logic. SL, 71(2):177-198, 2002. Google Scholar
  43. W.C. Purdy. Inexpressiveness of First-Order Fragments. AJL, 4:1-12, 2006. Google Scholar
  44. W.V. Quine. Variables Explained Away. PAPS, 104(3), 1960. Google Scholar
  45. I. Sain. Beth’s and Craig’s Properties via Epimorphisms and Amalgamation in Algebraic Logic. In ALUACS'88, LNCS 425, pages 209-225. Springer, 1990. Google Scholar
  46. S. Schewe. \ATLS Satisfiability is 2ExpTime-Complete. In ICALP'08, LNCS 5126, pages 373-385. Springer, 2008. Google Scholar
  47. S. Schewe and B. Finkbeiner. Satisfiability and Finite Model Property for the Alternating-Time muCalculus. In CSL'06, pages 591-605. Springer, 2006. Google Scholar
  48. S.G. Simpson. Partial Realizations of Hilbert’s Program. JSL, 53(2):349-363, 1988. Google Scholar
  49. B. ten Cate and L. Segoufin. Unary Negation. In STACS'11, LIPIcs 9, pages 344-355. Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  50. B. ten Cate and L. Segoufin. Unary Negation. LMCS, 9(3):1-46, 2013. Google Scholar
  51. J.D. Ullman. Principles of Database Systems. Computer Science Press, 1982. Google Scholar
  52. J. van Benthem. Dynamic Bits And Pieces. Technical report, University of Amsterdam, Amsterdam, Netherlands, 1997. Google Scholar
  53. J. van Benthem. Modal Logic In Two Gestalts. In AIML'98, pages 91-118. CSLI Publications, 2000. Google Scholar
  54. D. van Dalen. Logic and Structure (3rd ed.). Universitext. Springer, 1994. Google Scholar
  55. M.Y. Vardi. The Complexity of Relational Query Languages (Extended Abstract). In STOC'82, pages 137-146. Association for Computing Machinery, 1982. Google Scholar
  56. M.Y. Vardi. On the Complexity of Bounded-Variable Queries. In PODS'95, pages 266-276. Association for Computing Machinery, 1995. Google Scholar
  57. M.Y. Vardi. Why is Modal Logic So Robustly Decidable? In DCFM'96, pages 149-184. American Mathematical Society, 1996. Google Scholar
  58. D. Walther, C. Lutz, F. Wolter, and M. Wooldridge. \ATL Satisfiability is Indeed ExpTime-Complete. JLC, 16(6):765-787, 2006. 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