CIRQUENT CALCULUS SYSTEM CL8S VERSUS CALCULUS OF STRUCTURES SYSTEM SKSG FOR PROPOSITIONAL LOGIC

摘要

Cirquent calculus and calculus of structures are two approaches to proof theory. Both of them apply deep inference which modifies objects at any level rather than only around the root as is the case in sequent calculus. In this paper we compare the proof complexity of the cirquent calculus system CL8S and the calculus of structures system SKSg at the classical propositional level, and show that CL8S polynomially simulates SKSg.