Abstract
We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every constructive canonical system induces a class of non-deterministic Kripke-style frames, for which it is strongly sound and complete. This non-deterministic semantics is used to show that such a system always admits a strong form of the cut-elimination theorem, and for providing a decision procedure for such systems.
This research was supported by THE ISRAEL SCIENCE FOUNDATION (grant No 809-06).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avron, A.: Simple Consequence Relations. Information and Computation 92, 105–139 (1991)
Avron, A.: Gentzen-Type Systems, Resolution and Tableaux. Journal of Automated Reasoning 10, 265–281 (1993)
Avron, A.: A Nondeterministic View on Nonclassical Negations. Studia Logica 80, 159–194 (2005)
Avron, A.: Non-deterministic Semantics for Families of Paraconsistent Logics. In: Beziau, J.-Y., Carnielli, W., Gabbay, D.M. (eds.) Handbook of Paraconsistency. Studies in Logic, vol. 9, pp. 285–320. College Publications (2007)
Avron, A., Lev, I.: Canonical Propositional Gentzen-Type Systems. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 529–544. Springer, Heidelberg (2001)
Avron, A., Lev, I.: Non-deterministic Multiple-valued Structures. Journal of Logic and Computation 15, 24–261 (2005)
Belnap, N.D.: Tonk, Plonk and Plink. Analysis 22, 130–134 (1962)
Ciabattoni, A., Terui, K.: Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82, 95–119 (2006)
Fernandez, D.: Non-deterministic Semantics for Dynamic Topological Logic. Annals of Pure and Applied Logic 157, 110–121 (2009)
Gentzen, G.: Investigations into Logical Deduction. In: Szabo, M.E. (ed.) The Collected Works of Gerhard Gentzen, pp. 68–131. North Holland, Amsterdam (1969)
Gurevich, Y., Neeman, I.: The Logic of Infons, Microsoft Research Tech Report MSR-TR-2009-10 (January 2009)
Kripke, S.: Semantical Analysis of Intuitionistic Logic I. In: Crossly, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, pp. 92–129. North-Holland, Amsterdam (1965)
Prior, A.N.: The Runabout Inference Ticket. Analysis 21, 38–39 (1960)
Sundholm, G.: Proof theory and Meaning. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 9, pp. 165–198 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avron, A., Lahav, O. (2009). Canonical Constructive Systems. In: Giese, M., Waaler, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2009. Lecture Notes in Computer Science(), vol 5607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02716-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-02716-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02715-4
Online ISBN: 978-3-642-02716-1
eBook Packages: Computer ScienceComputer Science (R0)