Abstract
Modular cut-elimination is a particular notion of ”cut-elimination in the presence of non-logical axioms” that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a ”universal” modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. The failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Buss, S.: An Introduction to Proof Theory. In: Handbook of Proof Theory, pp. 1–78. Elsevier Science (1998)
Ciabattoni, A.: Automated Generation of Analytic Calculi for Logics with Linearity. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 503–517. Springer, Heidelberg (2004)
Ciabattoni, A., Terui, K.: Towards a semantic characterization of cut-elimination. Studia Logica 82(1), 95–119 (2006)
Gentzen, G.: Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift 39, 176–210, 405–431 (1934)
Lopez-Escobar, E.G.K.: On the Interpolation Theorem for the Logic of Constant Domains. J. Symb. Log. 46(1), 87–88 (1981)
Miller, D., Pimentel, E.: Using Linear Logic to Reason about Sequent Systems. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 2–23. Springer, Heidelberg (2002)
Pfenning, F.: Structural Cut Elimination: I. Intuitionistic and Classical Logic. Inf. Comput. 157, 84–141 (2000)
Restall, G.: An Introduction to Substructural Logics. Routledge, London (1999)
Schütte, K.: Beweistheorie. Springer, Heidelberg (1960)
Tait, W.W.: Normal derivability in classical logic. In: The Sintax and Semantics of infinitary Languages. LNM, vol. 72, pp. 204–236 (1968)
Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)
Terui, K.: Which Structural Rules Admit Cut Elimination? — An Algebraic Criterion. Journal of Symbolic Logic (to appear)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2000)
Zamanski, A., Avron, A.: Cut-Elimination and Quantification in Canonical Systems. Studia Logica 82(1), 157–176 (2006)
Zamanski, A., Avron, A.: Canonical gentzen-type calculi with (n,k)-ary quantifiers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 251–265. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciabattoni, A., Terui, K. (2006). Modular Cut-Elimination: Finding Proofs or Counterexamples. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_10
Download citation
DOI: https://doi.org/10.1007/11916277_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)