Abstract
We present a general method for providing Kripke semantics for the family of fully-structural multiple-conclusion propositional sequent systems. In particular, many well-known Kripke semantics for a variety of logics are easily obtained as special cases. This semantics is then used to obtain semantic characterizations of analytic sequent systems of this type, as well as of those admitting cut-admissibility. These characterizations serve as a uniform basis for semantic proofs of analyticity and cut-admissibility in such systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Avron, A.: On Modal Systems having arithmetical interpretations. Journal of Symbolic Logic 49, 935–942 (1984)
Avron, A.: Gentzen-Type Systems, Resolution and Tableaux. Journal of Automated Reasoning 10, 265–281 (1993)
Avron, A.: Classical Gentzen-type Methods in Propositional Many-Valued Logics. In: Fitting, M., Orlowska, E. (eds.) Beyond Two: Theory and Applications of Multiple-Valued Logic, Studies in Fuzziness and Soft Computing, vol. 114, pp. 117–155. Physica Verlag, Heidelberg (2003)
Avron, A.: A Non-Deterministic View on Non-Classical Negations. Studia Logica 80, 159–194 (2005)
Avron, A., Lahav, O.: On Constructive Connectives and Systems. Journal of Logical Methods in Computer Science 6 (2010)
Avron, A., Lev, I.: Non-deterministic Multiple-valued Structures. IJCAR 2001 15 (2005); Avron, A., Lev, I.: Canonical Propositional Gentzen-Type Systems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, p. 529. Springer, Heidelberg (2001)
Ciabattoni, A., Terui, K.: Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82, 95–119 (2006)
Crolard, T.: Subtractive Logic. Theoretical Computer Science 254, 151–185 (2001)
Goré, R., Postniece, L.: Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic. Journal of Logic and Computation 20(1), 233–260 (2010)
Gurevich, Y., Neeman, I.: The Infon Logic: the Propositional Case. To appear in ACM Transactions on Computation Logic 12 (2011)
Ono, H.: On some intuitionistic modal logic, pp. 687–722. Publications of Research Institute for Mathematical Sciences, Kyoto University (1977)
Pinto, L., Uustalu, T.: Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 295–309. Springer, Heidelberg (2009)
Sambin, G., Valentini, S.: The modal logic of provability. The sequential approach. Journal of Philosophical Logic 11, 311–342 (1982)
Takeuti, G.: Proof Theory. North-Holland, Amsterdam (1975)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996)
Rineke, V.: Provability Logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2010), http://plato.stanford.edu/entries/logic-provability/ (revision November 2010)
Wansing, H.: Sequent Systems for Modal Logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn. vol. 8, pp. 61–145 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avron, A., Lahav, O. (2011). Kripke Semantics for Basic Sequent Systems. In: Brünnler, K., Metcalfe, G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2011. Lecture Notes in Computer Science(), vol 6793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22119-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-22119-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22118-7
Online ISBN: 978-3-642-22119-4
eBook Packages: Computer ScienceComputer Science (R0)