From truth to computability I
arXiv:cs/0407054 · doi:10.1016/j.tcs.2006.03.014
Abstract
The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at http://www.cis.upenn.edu/~giorgi/cl.html . The present paper contains a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elementary-base fragment. Among the potential application areas for this result are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resource-bound planning and action. This paper is self-contained as it reintroduces all relevant definitions as well as main motivations.
To appear in Theoretical Computer Science
References in corpus (3)
Cited by in corpus (24)
- Sequential operators in computability logic
- Introduction to Cirquent Calculus and Abstract Resource Semantics
- Computability Logic: a formal theory of interaction
- The intuitionistic fragment of computability logic at the propositional level
- Intuitionistic computability logic
- From truth to computability II
- Many concepts and two logics of algorithmic reduction
- The taming of recurrences in computability logic through cirquent calculus, Part I
- Toggling operators in computability logic
- The logic of interactive Turing reduction
- From formulas to cirquents in computability logic
- Introduction to clarithmetic II
- Towards applied theories based on computability logic
- In the beginning was game semantics
- Introduction to clarithmetic I
- A logical basis for constructive systems
- A new face of the branching recurrence of computability logic
- On the system CL12 of computability logic
- The taming of recurrences in computability logic through cirquent calculus, Part II
- Separating the basic logics of the basic recurrences
- Elementary-base cirquent calculus I: Parallel and choice connectives
- Build your own clarithmetic I: Setup and completeness
- A PSPACE-Complete First Order Fragment of Computability Logic
- Implementing program extraction from CL1-proofs