A decision algorithm for the CL15 fragment of computability logic

Computability Logic (CoL) is a constructive and resource-conscious game semantical approach to interactive computability which captures dynamic and uncertain multi-agent interactions. By replacing the classical notion of truth with that of computability, CoL transitions from a classical logic of states to one of strategies, thus entailing a shift in the understanding of logical validity. In this framework, formulas are interpreted as interactive computational problems, i.e. games played between two pre-defined agents: Machine M, the honest player, and Environment E, the deceitful adversary. A formula is considered valid if there exists an effective strategy (an algorithm) for M to win the game against any possible behaviour of E. The question of decidability for several of expressive fragments of CoL has remained an open challenge in the last few years. This work focusses on the propositional fragment CL15, a system whose signature includes negation, parallel disjunction, parallel conjunction and branching recurrence operators. The core of the present contribution is the formulation of a decision algorithm for CL15.