Abstract
Let i, j ≥1, and let Σ\(^{i}_{j}\) denote the class of the higher order logic formulas of order i+1 with j–1 alternations of quantifier blocks of variables of order i+1, starting with an existential quantifier block. There is a precise correspondence between the non deterministic exponential time hierarchy and the different fragments of higher order logics Σ\(^{i}_{j}\), namely NEXP \(^{j}_{i}\) = Σ\(^{i+1}_{j}\). In this article we present a complete problem for each level of the non deterministic exponential time hierarchy, with a very weak sort of reductions, namely quantifier-free first order reductions. Moreover, we don’t assume the existence of an order in the input structures in this reduction. From the logical point of view, our main result says that every fragment Σ\(^{i}_{j}\) of higher order logics can be captured with a first order logic Lindström quantifier. Moreover, as our reductions are quantifier-free first order formulas, we get a normal form stating that each Σ\(^{i}_{j}\) sentence is equivalent to a single occurrence of the quantifier and a tuple of quantifier-free first order formulas. Our complete problems are a generalization of the well known problem quantified Boolean formulas with bounded alternation (QBF j ).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)
Balcázar, J., Díaz, J., Gabarró, J., Structural Complexity, I.: Structural Complexity I, 2nd edn. Springer, Heidelberg (1995)
Büchi, J.R.: Weak Second-Order Arithmetic and Finite Automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 6, 66–92 (1960)
Dahlhaus, E.: Reduction to NP-Complete Problems by Interpretations. In: Börger, E., Hasenjaeger, G., Rödding, D. (eds.) Logic and Machines: Decision Problems and Complexity. LNCS, vol. 171, pp. 357–365. Springer, Heidelberg (1984)
Dawar, A.: Generalized Quantifiers and Logical Reducibilities. Journal of Logic and Computation 5, 213–226 (1995)
Ebbinghaus, H., Flum, J.: Finite Model Theory, 2nd edn. Springer, Heidelberg (1999)
Fagin, R.: Generalized First Order Spectra and Polynomial Time Recognizable Sets. In: Karp, R. (ed.) Complexity of Computation. SIAM AMS Proceedings, vol. 7, pp. 43–73 (1974)
Grohe, M.: Complete Problems for Fixed-Point Logics. Journal of Symbolic Logic 60, 517–527 (1995)
Hull, R., Su, J.: On the Expressive Power of Database Queries with Intermediate Types. Journal of Computer and System Sciences 43(1), 219–267 (1991)
Hella, L., Turull Torres, J.M.: Expressibility of Higher Order Logics. Electronic Notes in Theoretical Computer Science 84 (2003)
Hella, L., Turull Torres, J.M.: Complete Problems for Higher Order Logics, Technical Report 12/2005, p. 27, Information Systems Department, Massey University (2005)
Hella, L., Turull Torres, J.M.: Computing Queries with Higher Order Logics. Theoretical Computer Science 355(2), 197–214 (2006)
Immerman, N.: Languages which Capture Complexity Classes. In: 15th ACM STOC Symposium, pp. 347–354 (1983); revised version: Languages that Capture Complexity Classes. SIAM Journal of Computing 16(4), 760–778 (1987)
Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)
Leivant, D.: Descriptive Characterizations of Computational Complexity. Journal of Computer and System Sciences 39, 51–83 (1989)
Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)
Stewart, I.: Comparing the Expressibility of Languages Formed Using NP-Complete Operators. Journal of Logic and Computation 1(3), 305–330 (1991)
Stockmeyer, L.: The Polynomial Time Hierarchy. Theoretical Computer Science 3(1), 1–22 (1976)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hella, L., Turull-Torres, J.M. (2006). Complete Problems for Higher Order Logics. In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_25
Download citation
DOI: https://doi.org/10.1007/11874683_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)