Study On Several Formal Systems And Operators For Computability Logic

Computability logic, introduced recently, is a formal theory of computability. It has interactive game semantics, and is a logic of resources. Classical, intuitionistic, and linear (in a broad sense) logics are just three special fragments of it. Unlike the more traditional logics, it has greater expressiveness and higher efficiency, which makes it be potentially used in knowledgebase systems, systems for planning and action, verifying circuit equivalence etc.Base on cirquent calculus, we devote our efforts to studying several formal systems and operators for computability loigc, and are summarizing as follows:· We prove the soundness and completeness of the cirquent calculus system CL6. First, a series of syntactic definitions, relevant to our proofs, are given; Then, based on the fact that system CL2is sound and complete w.r.t. the semantics of computability logic, we indirectly prove that system CL6is sound and complete w.r.t. this semantics, and hence get an extension of both classical propositional logic and cirquent calculus system CL5.· We discuss the relationship between the parallel recurrence and the uncountable branching recurrence. First, we give the cirquent calculus system on parallel recurrence; Then, we define the semantics of cirquent on parallel recurrence; Based on it, we prove the soundness of the system on parallel recurrence, and get that the logic induced by uncountable branching recurrence is a proper subset of the logic induced by parallel recurrence; Finally, we obtain that parallel recurrence is strictly weaker than uncountable branching recurrence, in the sense that the latter logically implies the former but not vise versa. As a result, the relationship between them is clearly known.· We discuss the relationship between the countable and uncountable branching recurrences. First, a new simplified definition of countable branching recurrence is given, and the equivalence between this new version and the old one is proven; After this new definition, the semantics of the cirquent on countable branching recurrence is defined, further, the soundness of the corresponding cirquent calculus system is proven; Then, we get that the logic induced by the uncountable branching recurrence is a proper subset of the logic induced by the countable one; Similarly to the previous work, we obtain that the countable branching recurrence is strictly weaker than the uncountable one, which makes their relationship thoroughly clear.· Based on the advantage of cirquent calculus, we give a compressed expression for classical propositional formula, and prove that the proof efficiency of the corresponding system for propositional logic is exponentially higher than that of the sequent calculus system Gentzen\{cut}. And hence, we provide for classical propositional logic a sound and complete formal system with higher proof efficiency. Further, we prove that the deduction theorem holds for the cirquent calculus system CL8S, compare the proof complexity of CL8S with that of the calculus of structures system SKSg at the classical propositional level, and show that CL8S polynomially simulates SKSg.· Given the superiority of the game semantics, we analyze the possibility and ad-vantages of computability logic’s being the underlying logic in knowledgebase systems. We express and inference knowledge based on the complete subset CL4of computability logic, provide the forward and backward reasoning, and give examples to show that this method has at least the merit of being more expressive and more convenient for interactive process.