The intuitionistic fragment of computability logic at the propositional level
Logic in Computer Science
2011-04-15 v2 Artificial Intelligence
Logic
Abstract
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.
Cite
@article{arxiv.cs/0602011,
title = {The intuitionistic fragment of computability logic at the propositional level},
author = {Giorgi Japaridze},
journal= {arXiv preprint arXiv:cs/0602011},
year = {2011}
}