Abstract: Computability or algorithm solvablity,is one of the important concepts in the field of mathematics and computer science.Computability logic (abbreviated as CoL) is a formal theory of computability and an interactive resource logic.CoL2 logic uses game semantics.CoL2 is an extension of classical propositional logic.What makes CoL2 more expressive than classical propositional logic is the presence of choice operators and general atom.CoL2 has a higher proof efficiency.In this paper,the decidability of CoL2 was presented,in other words,by presenting an algorithm whether any CoL2 formula is provable can be determined,and we proved that the algorithm runs in polynomial space.

Key words: Computability logic,CoL2,Interactive algorithms,Game semantics