2006/02/11 by Giorgi Japaridze · 4 citations
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.AI #cs.LO #math.LO
paper · pdf · doi:10.1016/j.apal.2007.05.001
published as Annals of Pure and Applied Logic 147 (2007), pp. 187-227
arxiv created 2006/02/11 · openalex publication_date 2007/05/24 · crossref created 2007/05/24 · crossref issued 2007/07/01 · crossref published 2007/07/01 · crossref published-print 2007/07/01 · arxiv updated 2011/04/15 · openalex created_date 2016/06/24 · crossref deposited 2019/04/28 · crossref indexed 2025/10/12 · openalex updated_date 2026/07/31
This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible -- and hence most natural -- sense, disjunction and conjunction as deterministic-choice combinations of problems (disjunction = machine's choice, conjunction = environment's choice), and "absurd" as a computational problem of universal strength. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.