Cited By
View all- Freire CMartins A(2019)The Descriptive Complexity of the Deterministic Exponential Time HierarchyElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2952797.2952921269:C(71-82)Online publication date: 5-Jan-2019
Fixed-Point Quantifiers in Higher Order Logics
Abstract
We add inflationary and non-inflationary fixed-points to higher-order logics. We show that, for every order, it is sufficient to increase the order of the given logic by one to capture inflationary fixed-points and by two to capture non-inflationary fixed-points. In the two cases, restricting to the existential fragment of the corresponding logic turns out to be enough. This also holds for non-deterministic fixed-points.
References
[1]
Abiteboul, S., R. Hull, and V. Vianu, Foundations of Databases , Addison-Wesley, 1994.
[2]
Abiteboul, S., Vardi, M. and Vianu, V., Fixed-Point Logics, Relational Machines, and Computational Complexity , Journal of ACM 44(1), pp. 30-56, 1997.
[3]
Balcázar, J., J. Díaz, and J. Gabarró, Structural Complexity I , Springer, 2nd. ed., 1995.
[4]
Chandra, A. K. and D. Harel, Computable Queries for Relational Data Bases , Journal of Computer and System Sciences 21(2), p. 156-178, 1980.
[5]
Ebbinghaus, H., and J. Flum, Finite Model Theory , Springer, 2nd. ed., 1999.
[6]
Fagin, R., Generalized First Order Spectra and Polynomial Time Recognizable Sets , in "Complexity of Computation, SIAM AMS Proceedings", ed. R. Karp, 7, 1974.
[7]
Hull, R., and J. Su, On the Expressive Power of Database Queries with Intermediate Types , Journal of Computer and System Sciences 43(1), 219-267, 1991.
[8]
Hella, L., Turull Torres, J. M., Expressibility of Higher Order Logics , Electronic Notes in Theoretical Computer Science, Vol. 84, 2003.
[9]
Immerman, N., Relational Queries Computable in Polynomial Time , Information and Control, 68: 86-104, 1986.
[10]
Leivant, D., Descriptive Characterizations of Computational Complexity , Journal of Computer and System Sciences 39(1), p. 51-83, 1989.
[11]
Vardi, M., The Complexity of Relational Query Languages , Proc. 14th ACM Symp. on Theory of Computing, p. 137-146, 1982.
- Fixed-Point Quantifiers in Higher Order Logics
Recommendations
Higher-order representation of substructural logics
ICFP '10We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, ...
Higher-order representation of substructural logics
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programmingWe present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, ...
Combining and automating classical and non-classical logics in classical higher-order logics
Numerous classical and non-classical logics can be elegantly embedded in Church's simple type theory, also known as classical higher-order logic. Examples include propositional and quantified multimodal logics, intuitionistic logics, logics for security,...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
IOS Press
Netherlands
Publication History
Published: 17 May 2006
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 01 Jan 2025
Other Metrics
Citations
Cited By
View all- Freire CMartins A(2019)The Descriptive Complexity of the Deterministic Exponential Time HierarchyElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2952797.2952921269:C(71-82)Online publication date: 5-Jan-2019