Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18 of the basic propositional fragment of computability logic the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical result of the article is a proof of the soundness and completeness of CL18 with respect to the semantics of computability logic.

翻译：Cirquent 演算是一种能够自然刻画逻辑表达式中子组件共享的证明系统。本文在其框架内，为可计算性逻辑的基本命题片段构建了一套公理化系统 CL18；可计算性逻辑是一种基于博弈语义、面向计算资源与任务的逻辑。该片段的非逻辑原子表示任意的所谓静态博弈，其逻辑词汇中的连接词包括否定、以及合取与析取的并行版本与选择版本。本文的主要技术成果是证明了 CL18 相对于可计算性逻辑语义的可靠性与完备性。