Intuitionistic computability logic

Japaridze Giorgi: Intuitionistic computability logic. In: Acta cybernetica, (18) 1. pp. 77-113. (2007)

[thumbnail of Japaridze_2007_ActaCybernetica.pdf]
Cikk, tanulmány, mű

Download (390kB) | Preview


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 formulas represent computational problems and "truth" is understood as algorithmic solvability, CL potentially offers a comprehensive logical basis for constructive applied theories and computing systems inherently requiring constructive and computationally meaningful underlying logics. Among the best known constructivistic logics is Heyting's intuitionistic calculus INT, whose language can be seen as a special fragment of that of CL. The constructivistic philosophy of INT, however, just like the resource philosophy of linear logic, has never really found an intuitively convincing and mathematically strict semantical justification. CL has good claims to provide such a justification and hence a materialization of Kolmogorov's known thesis "INT = logic of problems". The present paper contains a soundness proof for INT with respect to the CL semantics.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2007
Volume: 18
Number: 1
ISSN: 0324-721X
Page Range: pp. 77-113
Language: English
Event Title: Kalmár Workshop on Logic in Computer Science, 2003, Szeged
Related URLs:
Uncontrolled Keywords: Természettudomány, Informatika
Additional Information: Bibliogr.: p. 112-113.; Abstract
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2021. Mar. 24. 14:05

Actions (login required)

View Item View Item