research-article

The Complexity of Decomposing Modal and First-Order Theories

Authors:

Stefan Göller,

Jean-Christoph Jung,

Markus LohreyAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 16, Issue 1

Article No.: 9, Pages 1 - 43

https://doi.org/10.1145/2699918

Published: 24 March 2015 Publication History

Abstract

We study the satisfiability problem of the logic K² = K × K—the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998 that this problem is decidable in a tower of exponentials. So far, the best-known lower bound is NEXP-hardness shown by Marx and Mikulás in 2001.

Our first main result closes this complexity gap. We show that satisfiability in K² is nonelementary. More precisely, we prove that it is k-NEXP-complete, where k is the switching depth (the minimal modal rank among the two dimensions) of the input formula, hereby solving a conjecture of Marx and Mikulás. Using our lower-bound technique also allows us to derive nonelementary lower bounds for the two-dimensional modal logics K4 × K and S5₂ × K, for which only elementary lower bounds were previously known.

Moreover, we apply our technique to prove nonelementary lower bounds for the sizes of Feferman-Vaught decompositions with respect to product for any decomposable logic that is at least as expressive as unimodal K, generalizing a recent result by the first author and Lin. For the three-variable fragment FO³ of first-order logic, we obtain the following two immediate corollaries: the size of Feferman-Vaught decompositions with respect to disjoint sum are inherently nonelementary, and equivalent formulas in Gaifman normal form are inherently nonelementary.

Our second main result consists in providing effective elementary (more precisely, doubly exponential) upper bounds for the two-variable fragment FO² of first-order logic both for Feferman-Vaught decompositions and for equivalent formulas in Gaifman normal form.

References

[1]

P. Blackburn, M. de Rijke, and Y. Venema. 2001. Modal Logic. Cambridge University Press.

Digital Library

[2]

P. Blackburn, F. Wolter, and J. van Benthem (Eds.). 2006. Handbook of Modal Logic. Elsevier.

[3]

E. Börger, E. Grädel, and Y. Gurevich. 2001. The Classical Decision Problem. Springer-Verlag, Berlin, Heidelberg.

[4]

B. S. Chlebus. 1984. From domino tilings to a new model of computation. In Computation Theory. Lecture Notes in Computer Science, Vol. 208. Springer, 24--33.

[5]

A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. 2007. Model theory makes formulas large. In Automata, Languages and Programming. Lecture Notes in Computer Science, Vol. 4596. Springer, 913--924.

Digital Library

[6]

S. Feferman and R. L. Vaught. 1959. The first order properties of products of algebraic systems. Fundamenta Mathematicae 47, 57--103.

[7]

J. Flum and M. Grohe. 2006. Parametrized Complexity Theory. Springer.

Digital Library

[8]

D. Gabbay, A. Kurusz, F. Wolter, and M. Zakharyaschev. 2003. Many-Dimensional Modal Logics: Theory and Applications. Elsevier.

[9]

D. M. Gabbay and V. B. Shehtman. 1998. Products of modal logics, part 1. Logic Journal of the IGPL 6, 1, 73--146.

[10]

D. Gabelaia, A. Kurucz, F. Wolter, and M. Zakharyaschev. 2005. Products of ‘transitive’ modal logics. Journal of Symbolic Logic 70, 3, 993--1021.

[11]

H. Gaifman. 1982. On local and nonlocal properties. In Proceedings of the Herbrand Symposium, Logic Colloquium’81. 105--135.

[12]

S. Göller and A. W. Lin. 2012. Concurrency makes simple theories hard. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS’12). 344--355.

[13]

S. Göller, J. C. Jung, and M. Lohrey. 2012. The complexity of decomposing modal and first-order theories. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS’12). IEEE, Los Alamitos, CA, 325--334.

Digital Library

[14]

E. Grädel, P. G. Kolaitis, and M. Y. Vardi. 1997. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic 3, 1, 53--69.

[15]

J. Y. Halpern and M. Y. Vardi. 1989. The complexity of reasoning about knowledge and time. I. Lower bounds. Journal of Computer and System Sciences 38, 1, 195--237.

Digital Library

[16]

R. Hirsch, I. M. Hodkinson, and Á. Kurucz. 2002. On modal logics between K x K x K and S5 x S5 x S5. Journal of Symbolic Logic 67, 1, 221--234.

[17]

S. Kreutzer. 2009. Algorithmic meta-theorems. Electronic Colloquium on Computational Complexity 16, 147.

[18]

R. E. Ladner. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6, 3, 467--480.

[19]

J. A. Makowsky. 2004. Algorithmic uses of the Feferman-Vaught theorem. Annals of Pure and Applied Logic, 126, 1--3, 159--213.

[20]

M. Marx. 1999. Complexity of products of modal logics. Journal of Logic and Computation 9, 2, 197--214.

[21]

M. Marx and S. Mikulás. 2001. Products, or how to create modal logics of high complexity. Logic Journal of the IGPL 9, 1, 71--82.

[22]

M. Marx and Y. Venema. 1996. Multi-Dimensional Modal Logic. Kluwer Academic Press.

[23]

A. Mostowski. 1952. On direct products of theories. Journal of Symbolic Logic 17, 1--31.

[24]

A. Rabinovich. 2007. On compositionality and its limitations. ACM Transactions on Compututational Logic 8, 1.

Digital Library

Cited By

Kamdjoug JSando HKala JTeutio ATiwari SWamba S(2024)Data analytics-based auditing: a case study of fraud detection in the banking contextAnnals of Operations Research10.1007/s10479-024-06129-8Online publication date: 2-Jul-2024
https://doi.org/10.1007/s10479-024-06129-8
Kurucz AWolter FZakharyaschev MMarquis PSon TKern-Isberner G(2023)Definitions and (uniform) interpolants in first-order modal logicProceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2023/41(417-428)Online publication date: 2-Sep-2023
https://dl.acm.org/doi/10.24963/kr.2023/41
Sankaran A(2023)Feferman–Vaught Decompositions for Prefix Classes of First Order LogicJournal of Logic, Language and Information10.1007/s10849-022-09384-932:1(147-174)Online publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1007/s10849-022-09384-9
Show More Cited By

Index Terms

The Complexity of Decomposing Modal and First-Order Theories
1. Theory of computation
  1. Logic
  2. Models of computation
    1. Computability

Recommendations

The Complexity of Decomposing Modal and First-Order Theories
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science

We show that the satisfiability problem for the two-dimensional extension KxK of unimodal K is nonelementary, hereby confirming a conjecture of Marx and Mikulas from 2001. Our lower bound technique allows us to derive further lower bounds for many-...
Modal Hyperdoctrine: Higher-Order and Non-normal Extensions
Logic, Language, Information, and Computation
Abstract
Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic but are flexible enough to be applied to other logics and extended to higher-order systems. We return to Ghilardi’s hyperdoctrine semantics for first-order modal ...
The Ackermann approach for modal logic, correspondence theory and second-order reduction

The problem of eliminating second-order quantification over predicate symbols is in general undecidable. Since an application of second-order quantifier elimination is correspondence theory in modal logic, understanding when second-order quantifier ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 16, Issue 1

March 2015

246 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2670130

Editor:
Dale Miller
INRIA Saclay, France

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 March 2015

Accepted: 01 September 2014

Revised: 01 August 2014

Received: 01 December 2012

Published in TOCL Volume 16, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

DFG research project ProbDL (LU1417/1-1)
DFG research project GELO (LO 748/7-2)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
130
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kamdjoug JSando HKala JTeutio ATiwari SWamba S(2024)Data analytics-based auditing: a case study of fraud detection in the banking contextAnnals of Operations Research10.1007/s10479-024-06129-8Online publication date: 2-Jul-2024
https://doi.org/10.1007/s10479-024-06129-8
Kurucz AWolter FZakharyaschev MMarquis PSon TKern-Isberner G(2023)Definitions and (uniform) interpolants in first-order modal logicProceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2023/41(417-428)Online publication date: 2-Sep-2023
https://dl.acm.org/doi/10.24963/kr.2023/41
Sankaran A(2023)Feferman–Vaught Decompositions for Prefix Classes of First Order LogicJournal of Logic, Language and Information10.1007/s10849-022-09384-932:1(147-174)Online publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1007/s10849-022-09384-9
Bresolin DKurucz AMuñoz-Velasco ERyzhikov VSciavicco GZakharyaschev M(2017)Horn Fragments of the Halpern-Shoham Interval Temporal LogicACM Transactions on Computational Logic10.1145/310590918:3(1-39)Online publication date: 11-Aug-2017
https://dl.acm.org/doi/10.1145/3105909
Gutiérrez-Basulto VJung JSchneider T(2015)Lightweight temporal description logics with rigid roles and restricted TBoxesProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832581.2832670(3015-3021)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832581.2832670

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents