Analysis On Space Complexity Of COL1

In early 21st century, Giorgi Japaridze proposed the concept of computability logic (CoL), which is the interactive resource semantics. Computability logic is the combination of logic and computation theory. Unlike the classical logic used to tell us the truth of the proposition, the reseach goal of computability logic is to provide a system goal for discovering what is computable and how to calculate. The application fields of computability logic are not only about fundamental areas logic and computation theory, but also contain konwleage-based system and planning and behavior system and declarative programming language and automatic program generation and so on. Compared with classical logic, computability logic is a more strict mathematical semantics resouces, which is more expressive and more creativity. Computability logic also has more computing significance.In the same sense as Classical logic is a formal theory of truth, computability logic is a formal theory of computability. In computability logic, it understands computational problems as games palyed by a machine against environment. A problem is computable is that exists a machine that always wins the game. That is, this prolem has the property of computability. In computability, computable problems can be described in the form of formula, the logical operatiors of the formula represents the interactive operations between computer and environment. A formula is provable is that exists a method to solve the problem, in other words, exists a strategy to win the corresponding game. Therefore, computability logic is not only a kind of a special logic, but also the more challenged project from the truth to computability.This paper discussed CoL1 system of computability logic, which uses the game semantics. CoL1 is an extension of classical propositional logic. What makes CoL1 more expressive than CoLassical propositional logic is the presence of choice operator (which is introduced in the second chapter).In this paper, the formal definition of game is introduced, and interpretes though the examples. Then introduces the logical operations involved in CoL1, such as the negative operation and selection operation and parallel operationand and reduction operation, and also illustrate these operations by the chess model. Then given the concept of static game, and introduces two kinds of interactive computing model, HPM and EPM, which achieve the computer strategy though the valid computer program. For HPM, the operation of environment can be arbitrarily, but for EPM, only when computer is in the granting permission, can the environment operate. In the third chapter, the syntax, semantics and rules of CoL1 system is introduced and the simple proof of soundness and completeness of the CoL1 system is given, and also introduce several theorems in CoLl system. Finally, we analyze the space complexity of CoLl. As the space complexity of quantified boolean formula is PSPACE complete, and the space complexity of the provability of CoL1 formula is also PSPACE, therefore, though construct a mapping reduction from quantified boolean formula to the provability of CoLl formula, that CoLl is PSPACE complete can be proved.