The intuitionistic fragment of computability logic at the propositional level
<|reference_start|>The intuitionistic fragment of computability logic at the propositional level: 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.<|reference_end|>
@article{japaridze2006the,
    title={The intuitionistic fragment of computability logic at the propositional
  level},
    author={Giorgi Japaridze},
    journal={Annals of Pure and Applied Logic 147 (2007), pp. 187-227},
    year={2006},
    doi={10.1016/j.apal.2007.05.001},
    archivePrefix={arXiv},
    eprint={cs/0602011},
    primaryClass={cs.LO cs.AI math.LO}
}