Kripke semantics for basic sequent systems. (English) Zbl 1333.03236
Brünnler, Kai (ed.) et al., Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4–8, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22118-7/pbk). Lecture Notes in Computer Science 6793. Lecture Notes in Artificial Intelligence, 43-57 (2011).
Summary: 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.
For the entire collection see [Zbl 1216.68022].
For the entire collection see [Zbl 1216.68022].
References:
| [1] | Avron, A.: On Modal Systems having arithmetical interpretations. Journal of Symbolic Logic 49, 935–942 (1984) · Zbl 0587.03016 · doi:10.2307/2274147 |
| [2] | Avron, A.: Gentzen-Type Systems, Resolution and Tableaux. Journal of Automated Reasoning 10, 265–281 (1993) · Zbl 0788.03013 · doi:10.1007/BF00881838 |
| [3] | 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) · Zbl 1046.03011 · doi:10.1007/978-3-7908-1769-0_5 |
| [4] | Avron, A.: A Non-Deterministic View on Non-Classical Negations. Studia Logica 80, 159–194 (2005) · Zbl 1086.03023 · doi:10.1007/s11225-005-8468-5 |
| [5] | Avron, A., Lahav, O.: On Constructive Connectives and Systems. Journal of Logical Methods in Computer Science 6 (2010) · Zbl 1213.03069 |
| [6] | 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) · Zbl 0988.03011 |
| [7] | Ciabattoni, A., Terui, K.: Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82, 95–119 (2006) · Zbl 1105.03057 · doi:10.1007/s11225-006-6607-2 |
| [8] | Crolard, T.: Subtractive Logic. Theoretical Computer Science 254, 151–185 (2001) · Zbl 0983.03047 · doi:10.1016/S0304-3975(99)00124-3 |
| [9] | 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) · Zbl 1189.03070 · doi:10.1093/logcom/exn067 |
| [10] | Gurevich, Y., Neeman, I.: The Infon Logic: the Propositional Case. To appear in ACM Transactions on Computation Logic 12 (2011) · Zbl 1328.03032 |
| [11] | Ono, H.: On some intuitionistic modal logic, pp. 687–722. Publications of Research Institute for Mathematical Sciences, Kyoto University (1977) · Zbl 0373.02026 |
| [12] | 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) · Zbl 1260.03105 · doi:10.1007/978-3-642-02716-1_22 |
| [13] | Sambin, G., Valentini, S.: The modal logic of provability. The sequential approach. Journal of Philosophical Logic 11, 311–342 (1982) · Zbl 0523.03014 · doi:10.1007/BF00293433 |
| [14] | Takeuti, G.: Proof Theory. North-Holland, Amsterdam (1975) |
| [15] | Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) · Zbl 0868.03024 |
| [16] | 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) |
| [17] | 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) · doi:10.1007/978-94-010-0387-2_2 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
