Matthew S. Bauer
Abstract
In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to describe what can be computed, but also provide a mechanism for extracting computational algorithms from proofs. Among the most expressive and fundamental of these is CL4, known to be (constructively) sound and complete with respect to the underlying computational semantics. Furthermore, the ∀, ∃-free fragment of CL4 was shown to be decidable in polynomial space. The present work extends this result and proves that this fragment is, in fact, PSPACE-complete.
- Andreas Blass. 1992. A game semantics for linear logic. Ann. Pure Appl. Logic 56, 183--220.Google Scholar
Cross Ref
- Jaakko Hintikka. 1996. The Principles of Mathematics Revisited. Cambridge University Press, New York, NY. Google ScholarDigital Library
- Giorgi Japaridze. 2003. Introduction to computability logic. Ann. Pure Appl. Logic 123, 1--99.Google ScholarCross Ref
- Giorgi Japaridze. 2006a. From truth to computability I. Theor. Comput. Sci. 357, 1, 100--135. DOI: http://dx.doi.org/10.1016/j.tcs.2006.03.014 Google ScholarDigital Library
- Giorgi Japaridze. 2006b. Introduction to cirquent calculus and abstract resource semantics. J. Log. Comput. 16, 4, 489--532. DOI: http://dx.doi.org/10.1093/logcom/exl005 Google ScholarDigital Library
- Giorgi Japaridze. 2006c. Propositional computability logic I. ACM Trans. Comput. Logic 7, 2, 302--330. DOI: http://dx.doi.org/10.1145/1131313.1131318 Google ScholarDigital Library
- Giorgi Japaridze. 2006d. Propositional computability logic II. ACM Trans. Comput. Logic 7, 2, 331--362. DOI: http://dx.doi.org/10.1145/1131313.1131319 Google ScholarDigital Library
- Giorgi Japaridze. 2007. From truth to computability II. Theor. Comput. Sci. 379, 1--2, 20--52. DOI: http://dx.doi.org/10.1016/j.tcs.2007.01.004 Google ScholarDigital Library
- Giorgi Japaridze. 2009a. In the beginning was game semantics. In Games: Unifying Logic, Language and Philosophy, Ondrej Majer, Tero Tulenheimo, and Ahti-Veikko Pietarinen, Eds., Springer, Chapter 11, 249--235.Google Scholar
- Giorgi Japaridze. 2009b. Ptarithmetic. CoRR abs/0902.2969 (2009).Google Scholar
- Giorgi Japaridze. 2010a. Introduction to clarithmetic II. CoRR abs/1004.3236 (2010).Google Scholar
- Giorgi Japaridze. 2010b. Introduction to clarithmetic III. CoRR abs/1008.0770 (2010).Google Scholar
- Giorgi Japaridze. 2011a. Introduction to clarithmetic I. Inf. Comput. 209, 10, 1312--1354. DOI: http://dx.doi.org/10.1016/j.ic.2011.07.002 Google ScholarDigital Library
- P. Lincoln and A. Scedrov. 1992. First-order linear logic without modalities is NEXPTIME-hard. Theor. Comput. Sci. 135, 1, 139--153. DOI: http://dx.doi.org/10.1016/0304-3975(94)00107-3 Google ScholarDigital Library
- Michael Sipser. 2006. Introduction to the Theory of Computation (2nd Ed.). Thomson Course Technology, Boston, MA.Google Scholar
- Wenyan Xu and Sanyang Liu. 2012. Soundness and completeness of the cirquent calculus system CL6 for computability logic. Logic J. IGPL 20, 317--330.Google ScholarCross Ref
Index Terms
- A PSPACE-complete first-order fragment of computability logic
Recommendations
Propositional computability logic I
In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine against ...
Intuitionistic computability logic
Computability logic (CL) is a systematic formal theory of computational tasks and resources, which, in a sense, can be seen as a semantics-based alternative to (the syntactically introduced) linear logic. With its expressive and flexible language, where ...
From truth to computability II
Computability logic is a formal theory of computational tasks and resources. Formulas in it represent interactive computational problems, and ''truth'' is understood as algorithmic solvability. Interactive computational problems, in turn, are defined as ...
Comments