Document Open Access Logo

On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics

Authors Bartosz Bednarczyk , Maja Orłowska, Anna Pacanowska, Tony Tan

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.36.pdf
  • Filesize: 0.93 MB
  • 15 pages

Document Identifiers

Author Details

Bartosz Bednarczyk
  • Computational Logic Group, Technische Universität Dresden, Germany
  • Institute of Computer Science, University of Wrocław, Poland
Maja Orłowska
  • Institute of Computer Science, University of Wrocław, Poland
Anna Pacanowska
  • Institute of Computer Science, University of Wrocław, Poland
Tony Tan
  • Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan

Funding

  • Bednarczyk, Bartosz: supported by "Diamentowy. Grant" no. DI2017 006447.
  • Tan, Tony: supported by Taiwan Ministry of Science and Technology under grant no. 109-2221-E-002-143-MY3 and National Taiwan University under grant no. 109L891808.

Cite As Get BibTex

Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, and Tony Tan. On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSTTCS.2021.36

Abstract

During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning.
In this work we investigate the extensions of these classical decidable logics with percentage quantifiers, specifying how frequently a formula is satisfied in the indented model. We show, surprisingly, that all the mentioned decidable fragments become undecidable under such extension, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics, e.g. Presburger Modal Logics with Converse or ALCI, with expressive cardinality constraints.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and databases
Keywords
  • statistical reasoning
  • knowledge representation
  • satisfiability
  • fragments of first-order logic
  • guarded fragment
  • two-variable fragment
  • (un)decidability

Metrics

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

Related Versions

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal Languages and Bounded Fragments of Predicate Logic. J. Philosophical Logic, 1998. Google Scholar
  2. Franz Baader. A new description logic with set constraints and cardinality constraints on role successors. In Clare Dixon and Marcelo Finger, editors, FroCoS, 2017. Google Scholar
  3. Franz Baader, Bartosz Bednarczyk, and Sebastian Rudolph. Satisfiability checking and conjunctive query answering in description logics with global and local cardinality constraints. In DL, 2019. Google Scholar
  4. Franz Baader, Bartosz Bednarczyk, and Sebastian Rudolph. Satisfiability and query answering in description logics with global and local cardinality constraints. In ECAI, 2020. Google Scholar
  5. Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. Google Scholar
  6. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. J. ACM, 2015. Google Scholar
  7. Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, and Tony Tan. On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics. CoRR, abs/2106.15250, 2021. URL: http://arxiv.org/abs/2106.15250.
  8. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. In ICALP 2020, 2020. Google Scholar
  9. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  10. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In ICALP, 2016. Google Scholar
  11. Stéphane Demri and Denis Lugiez. Complexity of modal logics with presburger constraints. J. Appl. Log., 2010. Google Scholar
  12. Eric Domenjoud. Solving systems of linear diophantine equations: An algebraic approach. In MFCS, 1991. Google Scholar
  13. Seymour Ginsburg and Edwin Henry Spanier. Semigroups, presburger formulas, and languages. Pac. J. of Math., 16:285-296, 1966. Google Scholar
  14. Erich Grädel. Description logics and guarded fragments of first order logic. In DL, 1998. Google Scholar
  15. Erich Grädel. On the restraining power of guards. J. Symb. Log., 1999. Google Scholar
  16. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 1997. Google Scholar
  17. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In LICS, 1997. Google Scholar
  18. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. Arch. Math. Log., 1999. Google Scholar
  19. Yevgeny Kazakov. A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment. In JELIA, volume 3229 of LNCS, 2004. Google Scholar
  20. Clemens Kupke and Dirk Pattinson. On modal logics of linear inequalities. In Lev D. Beklemishev, Valentin Goranko, and Valentin B. Shehtman, editors, AIML, 2010. Google Scholar
  21. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. Google Scholar
  22. Yuri V. Matiyasevich. Hilbert’s Tenth Problem. MIT Press, 1993. Google Scholar
  23. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. Complexity results for first-order two-variable logic with counting. SIAM J. Comput., 29(4):1083-1117, 2000. Google Scholar
  24. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. Google Scholar
  25. Loic Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In RTA, 1991. Google Scholar
  26. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. J. Log. Lang. Inf., 14(3):369-395, 2005. Google Scholar
  27. Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. J. Log. Comput., 17(1):133-155, 2007. Google Scholar
  28. Dana Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 1962. Google Scholar
  29. B. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. In Proc. USSR Acad. Sci., volume 70(4), pages 569-572, 1950. Google Scholar
  30. Willard van Orman Quine. The Ways of Paradox and Other Essays, Revised Edition. Harvard University Press, 1976. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact