Abstract
Analytic tableau systems for the family of non-deterministic semantics are introduced. These are based on tableaux for many-valued logics using sets-as-signs DNF representations. Karnaugh maps illustrate the construction of tableau rules. In contrast to classical many-valued tableaux, we add a rule called sign intersection. Soundness and completeness are shown. As an example demonstrates, some tableau systems would be incomplete without sign intersection. There is a correspondence to well-studied canonical calculi based on sequent systems: Tableau systems can be translated into canonical calculi, but not vice-versa (structural rules are missing on the tableau side).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Also note that a tableau system for a particular non-deterministic semantics is already listed in [19, p. 211]. Unfortunately, we could not find out more about it; an approach to contact the author was unsuccessful.
- 2.
A usage of this nmatrix in a meaningful logic would be nice but is not intended.
References
Avron, A., Arieli, O., Zamansky, A.: Theory of Effective Propositional Paraconsistent Logics. College Publications (2018)
Avron, A., Konikowska, B.: Multi-valued calculi for logics based on non-determinism. Log. J. IGPL 13(4), 365–387 (2005). https://doi.org/10.1093/jigpal/jzi030
Avron, A., Lev, I.: Canonical propositional Gentzen-type systems. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 529–544. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_45
Avron, A., Lev, I.: Non-deterministic multiple-valued structures. J. Log. Comput. 15(3), 241–261 (2005). https://doi.org/10.1093/logcom/exi001
Avron, A., Zamansky, A.: Canonical signed calculi, non-deterministic matrices and cut-elimination. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 31–45. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92687-0_3
Avron, A., Zamansky, A.: Non-deterministic semantics for logical systems. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 16, 2nd edn, pp. 227–304. Springer, Heidelberg (2011). https://doi.org/10.1007/978-94-007-0479-4_4
Baaz, M., Fermüller, C.G., Salzer, G.: Automated deduction for many-valued logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, chap. 19, pp. 1355–1402. Elsevier and MIT Press (2001)
Baaz, M., Fermüller, C.G., Zach, R.: Dual systems of sequents and tableaux for many-valued logics. Bull. EATCS 51, 192–197 (1993)
Baaz, M., Lahav, O., Zamansky, A.: Finite-valued semantics for canonical labelled calculi. J. Autom. Reason. 51(4), 401–430 (2013). https://doi.org/10.1007/s10817-013-9273-x
Beckert, B., Hähnle, R., Manyà, F.: The SAT problem of signed CNF formulas. In: Basin, D., D’Agostino, M., Gabbay, D.M., Matthews, S., Viganò, L. (eds.) Labelled Deduction. APLS, vol. 17, pp. 59–80. Springer, Dordrecht (2000). https://doi.org/10.1007/978-94-011-4040-9_3
Carnielli, W.A.: Systematization of finite many-valued logics through the method of tableaux. J. Symb. Log. 52(2), 473–493 (1987). https://doi.org/10.2307/2274395
Coniglio, M.E., del Cerro, L.F., Newton, M.P.: Modal logic with non-deterministic semantics: part I–propositional case. Log. J. IGPL 28(3), 281–315 (2020). https://doi.org/10.1093/jigpal/jzz027
D’Agostino, M., Mondadori, M.: The taming of the cut. Classical refutations with analytic cut. J. Log. Comput. 4(3), 285–319 (1994). https://doi.org/10.1093/logcom/4.3.285
Fermüller, C.G.: On matrices, Nmatrices and games. J. Log. Comput. 26(1), 189–211 (2016). https://doi.org/10.1093/logcom/ext024
Hähnle, R.: Advanced many-valued logics. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 2, 2nd edn, pp. 297–395. Springer, Dordrecht (2001). https://doi.org/10.1007/978-94-017-0452-6_5
Hähnle, R.: Towards an efficient tableau proof procedure for multiple-valued logics. In: Börger, E., Kleine Büning, H., Richter, M.M., Schönfeld, W. (eds.) CSL 1990. LNCS, vol. 533, pp. 248–260. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54487-9_62
Hähnle, R.: Automated Deduction in Multiple-valued Logics. Oxford University Press (1993)
Hähnle, R.: Tableaux for many-valued logics. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 529–580. Kluwer (1999)
Ivlev, J.V.: Modal’naja logika. Moskovskogo Univ, Izdat (1991). (in Russian)
Konikowska, B.: Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculus. J. Appl. Non-Classical Log. 3(1), 39–71 (1993). https://doi.org/10.1080/11663081.1993.10510795
Ohnishi, M., Matsumoto, K.: A system for strict implication. Ann. Jpn. Assoc. Philos. Sci. 2(4), 183–188 (1964). https://doi.org/10.4288/jafpos1956.2.183
Omori, H., Skurt, D.: More modal semantics without possible worlds. IfCoLog J. Log. Appl. 3(5), 815–846 (2016)
Paoli, F.: Substructural Logics: A Primer. Trends in Logic. Kluwer Academic Publishers (2002)
Pawlowski, P.: Tree-like proof systems for finitely-many valued non-deterministic consequence relations. Log. Univers. 14(4), 407–420 (2020). https://doi.org/10.1007/s11787-020-00263-0
Rosser, J.B., Turquette, A.R.: Many-Valued Logics. North-Holland (1952)
Rouseau, G.: Sequents in many valued logic I. Fundam. Math. 60(1), 23–33 (1967). https://doi.org/10.4064/fm-60-1-23-33
Smullyan, R.M.: First-Order Logic. Dover, 2 edn. (1995)
Surma, S.J.: An algorithm for axiomatizing every finite logic. In: Rine, D.C. (ed.) Computer Science and Multiple-Valued Logic, pp. 137–143. North-Holland Publishing Company (1977)
Zamansky, A., Avron, A.: Canonical signed calculi with multi-ary quantifiers. Ann. Pure Appl. Logic 163(7), 951–960 (2012). https://doi.org/10.1016/j.apal.2011.09.006
Acknowledgements
I am indebted to Peter Steinacker for the supervision of my master’s thesis and to Andreas Maletti, second reviewer, for spotting the mistake in my thesis which initiated the work on the present paper. I would like to thank Daniel Skurt, Hitoshi Omori, Reiner Hähnle, Richard Bubel, Elio La Rosa, Pawel Pawlowski for useful suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Grätz, L. (2021). Analytic Tableaux for Non-deterministic Semantics. In: Das, A., Negri, S. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021. Lecture Notes in Computer Science(), vol 12842. Springer, Cham. https://doi.org/10.1007/978-3-030-86059-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-86059-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-86058-5
Online ISBN: 978-3-030-86059-2
eBook Packages: Computer ScienceComputer Science (R0)