From truth to computability I
<|reference_start|>From truth to computability I: 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.<|reference_end|>
@article{japaridze2004from,
    title={From truth to computability I},
    author={Giorgi Japaridze},
    journal={Theoretical Computer Science 357 (2006), pp. 100-135},
    year={2004},
    doi={10.1016/j.tcs.2006.03.014},
    archivePrefix={arXiv},
    eprint={cs/0407054},
    primaryClass={cs.LO cs.AI cs.GT math.LO}
}