Graduate studies at Western
Studia Logica 82 (1):51 - 71 (2006)
|Abstract||Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations.|
|Keywords||cut elimination deep inference first-order predicate logic|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.
Branislav R. Boričić (1986). A Cut-Free Gentzen-Type System for the Logic of the Weak Law of Excluded Middle. Studia Logica 45 (1):39 - 53.
Linda Postniece, Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Georg Moser & Richard Zach (2006). The Epsilon Calculus and Herbrand Complexity. Studia Logica 82 (1):133 - 155.
Sara Negri & Jan Von Plato (1998). Cut Elimination in the Presence of Axioms. Bulletin of Symbolic Logic 4 (4):418-435.
Phiniki Stouppa (2007). A Deep Inference System for the Modal Logic S. Studia Logica 85 (2):199 - 214.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Added to index2009-01-28
Total downloads3 ( #214,063 of 740,197 )
Recent downloads (6 months)1 ( #61,960 of 740,197 )
How can I increase my downloads?