A Local System for Classical Logic

Abstract. The calculus of structures is a framework for specifying logical systems, which is similar to the one-sided sequent calculus but more general. We present a system of inference rules for propositional classical logic in this new framework and prove cut elimination for it. The system enjoys a decomposition theorem for derivations that is not available in the sequent calculus. The main novelty of our system is that all the rules are local: contraction, in particular, is reduced to atomic form. This should be interesting for distributed proof-search and also for complexity theory, since the computational cost of applying each rule is bounded.

• Type: Conference
• Year: 2001
• Where: LPAR
• Authors: Kai Brünnler, Alwen Fernanto Tiu
• Keywords: Automated Reasoning, LPAR 2001, One-sided Sequent Calculus, Propositional Classical Logic, Sequent Calculus