On decidability and bounded proofs in fragments of computability logic

Computability logic (CoL) reinterprets logic as a formal theory of dynamic interaction, modelling statements as computational games between predefined agents M and E. The present work tackles two open problems regarding CoL fragments CL15 and CL5. Firstly, we prove CL15 decidable: the potentially infinite search space from resource contraction can be pruned while preserving completeness, bounding contraction applications through a function of the cirquent’s complexity. Secondly, we develop a novel and purely syntactic proof that any derivable cirquent in the duplication-free version of CL5 admits a polynomial-size derivation, bounded by three structural limits (width, branch length and node size) in the bottom-up proof construction.