Research On Decidablity And Space Complexity Of CL2in Computability Logic

Computability or algorithm solvablity, is one of the most important concepts in the field of mathematics and computer science. Computability logic (abbreviated as CoL) is a formal theory of computability. It understands computational problems as games played by a machine against its environment. Computability of the problem is the existence of a machine can always win the game. Computability logic is a formal theory of computability in the same sense as classical logic is a formal theory of truth. Formulas in CoL represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as its being a scheme of problems that always have algorithmic solutions (or, equivalently, there are strategies to win the game).The article first introduces the game semantics and its formal definition of computability logic, and gives the meaning and formal definition logical operators. Games consist of static games and dynamic games. Static game is a special kind of game. Intuitively, static games are ones where speed is irrelevant:in order to win, for either player only matters what to do (strategy) rather than how fast to do (speed). We are concerned only with the static game. The HPM (hard-play machine) is the basic model of the interactive computer model. It is a version of Turing machine. An EPM (easy-play machine) is another kind of interactive computer model, with the only difference that the environment can make a move only when the machine explicitly allows it to do so. For static game, these two models are equivalent. The actual problem-solving process, we prefer to adopt the EPM model.CL2logic uses game semantics, and it is a conservative extension of classical propositional logic, with the richer expressive, broader application prospects and have a higher proof of efficiency. Compared with the classical propositional logic, CL2logic contains two types of atoms:elementary atoms and general atoms. The elementary atoms stand for simple problems, corresponding to classical propositional logic predicates; the general atoms stand for the general problem of interactive computing, its meaning is different from the predicate. The concept of truth in classical logic is similar to validity in computability logic. The CL2logic has been proved to be a complete, reliable logic system.The main contributions of this thesis are as following: (l).We analysis the decidability of CL2logic. We illustrate the algorithm of determining validity (provability) of CL2-fomulas.. and prove that the algorithm runs in polynomial space.(2) We analysis of the space complexity of CL2logic. To show that CL2probability is PSPACE-Complete, we construct a polynomial time mapping reduction from QBF(Quantified Boolean Formula shorthand for the QBF) to CL2-provability. The result shows that it is harder than NP-hard problems.