Skip to main content
SpringerLink
Log in

Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving

  • Chapter
Beyond Two: Theory and Applications of Multiple-Valued Logic

Part of the book series: Studies in Fuzziness and Soft Computing ((STUDFUZZ,volume 114))

Abstract

We give a uniform presentation of representation and decidability results related to the Kripke-style semantics of several non-classical logics. We show that a general representation theorem (which has as particular instances the representation theorems as algebras of sets for Boolean algebras, distributive lattices and semi-lattices) extends in a natural way to several classes of operators and allows to establish a relationship between algebraic and Kripke-style models. We illustrate the ideas on several examples. We conclude by showing how the Kripke-style models thus obtained can be used (if first-order axiomatizable) for automated theorem proving by resolution for some non-classical logics.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson, A.R. and Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, volume 1. Princeton University Press, Princeton (1975)

    MATH  Google Scholar 

  2. Allwein, G. and Dunn, J.M.: Kripke models for linear logic. Journal of Symbolic Logic, 58, (2) (1993) 514 - 545

    Article  MathSciNet  MATH  Google Scholar 

  3. Andréka, H., van Benthem, J. and Németi, I.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27 (1998) 217 - 274

    Article  MathSciNet  MATH  Google Scholar 

  4. Blok, W.J. and Ferreirim, I.M.A.: On the structure of hoops. Algebra Universalis, 43 (2000) 233 - 257

    Article  MathSciNet  MATH  Google Scholar 

  5. Blyth, T.S. and Varlet, J.C.: Ockham Algebras. Oxford Science Publications (1994)

    Google Scholar 

  6. Brink, C.: Multisets and the algebra of relevance logic. The Journal of Nonclassical logic, 5 (1988) 75 - 95

    MathSciNet  Google Scholar 

  7. Clark, D.M. and Davey, B.A.: Natural dualities for the working algebraist, volume 57 of Cambridge studies in advanced mathematics Cambridge University Press, 1st edition (1998)

    Google Scholar 

  8. Davey, B.: Duality theory on ten dollars a day. In Rosenberg, I.G. and Sabidussi, G. editors, Algebras and Orders (Proceedings of the NATO ASI and Séminaire de mathématiques supérieures on Algebras and Orders, Montréal, Canada, July 29-August 9, 1991, NATO ASI Series, Vol. 389 (1993) 71 - 111

    Google Scholar 

  9. Davey, B.A. and Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press (1990)

    Google Scholar 

  10. Dos’en, K.: A historical introduction to substructural logics. In SchroederHeister P. and Dosen, K. editors, Substructural logics, Studies in Logic and Computation 2. Oxford Science Publisher (1993) 63 - 108

    Google Scholar 

  11. Dummet, M.: A propositional calculus with denumerable matrix. The Journal of Symbolic Logic, 24, (2) (1959) 97 - 106

    Article  MathSciNet  Google Scholar 

  12. Dunn, J.M.: Partial gaggles applied to logics with restricted structural rules. In Schroeder-Heister, P. and Dosen, K. editors, Substructural logics, Studies in Logic and Computation 2. Oxford Science Publisher (1993) 63 - 108

    Google Scholar 

  13. Dunn, J.M.: Positive modal logic. Studia Logica, 55 (1995) 301 - 317

    Article  MathSciNet  MATH  Google Scholar 

  14. Fitch, F.B.: A system of formal logic without an analogue to the Curry W operator. The Journal of Symbolic Logic, 1 (1936) 92 - 100

    Article  MATH  Google Scholar 

  15. Fitting, M.C.: Intuitionistic logic model theory and forcing. Studies in logic and the foundations of mathematics. North-Holland Publishing Company, Amsterdam (1969)

    Google Scholar 

  16. Fleischer, I.: Every BCK-algebra is a set of residuables in an integral pomonoid. Journal of Algebra, 119 (1988) 360 - 365

    Article  MathSciNet  MATH  Google Scholar 

  17. Gabbay, D.: Expressive functional completeness in tense logics. In Mönnich, U. editor, Aspects of Philosophical Logic. Reidel (1981) 91 - 117

    Google Scholar 

  18. Ganzinger, H., Hustadt, U., Meyer, Ch. and Schmidt, R.A.: A resolution-based decision procedure for extensions of K4. In Zakharyaschev, M., Segerberg, K., de Rijke, M. and Wansing, H. editors, Advances in Modal Logic, Volume 2, volume 119 of CSLI Lecture Notes, chapter 9. CSLI, Stanford, USA (2001) 225 - 246

    Google Scholar 

  19. Ganzinger, H., Meyer, C. and Veanes, M. The two-variable guarded fragment with transitive relations. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1999) 24 - 34

    Google Scholar 

  20. Gehrke, M.: Personal communication (2001)

    Google Scholar 

  21. Gehrke, M. and Priestley, H.A.: Non-canonicity of MV-algebras. Houston Journal of Mathematics. To appear.

    Google Scholar 

  22. Viorica Sofronie-Stokkermans

    Google Scholar 

  23. Gehrke, M. and Harding, J.: Bounded lattice expansions. Journal of Algebra, 238 (2001) 345 - 371

    Article  MathSciNet  MATH  Google Scholar 

  24. Gehrke, M. and Jônsson, B.: Bounded distributive lattices with operators. Mathematica Japonica, 40, (2) (1994) 207 - 215

    MathSciNet  MATH  Google Scholar 

  25. Gehrke, M. and Jônsson, B.: Monotone bounded distributive lattice expansions. Mathematica Japonica, 52, (2) (2000) 197 - 213

    MathSciNet  MATH  Google Scholar 

  26. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift (1935)

    Google Scholar 

  27. Girard, J.-Y.: Linear logic. Theoretical Computer Science (1987)

    Google Scholar 

  28. Grädel, E., Kolaitis, P. and Vardi, M.: On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3, (1) (1997) 53 - 69

    Article  MathSciNet  MATH  Google Scholar 

  29. Goldblatt, R.: Semantic analysis of orthologic. Journal of Philosophical Logic, 3 (1974) 19 - 35

    Article  MathSciNet  Google Scholar 

  30. Goldblatt, R.: Orthomodularity is not elementary. The Journal of Symbolic Logic, 49 (1984) 401 - 404

    Article  MathSciNet  MATH  Google Scholar 

  31. Goldblatt, R.: Varieties of complex algebras. Annals of Pure and Applied Logic, 44, (3) (1989) 153 - 301

    Article  MathSciNet  Google Scholar 

  32. Goldblatt, R.: Mathematics of modality, volume 43 of Center for the Study of Language and Information. Univ. of Chicago Press (1993)

    Google Scholar 

  33. Goldblatt, R.: Algebraic polymodal logic: A survey. Logic Journal of the IGPL, 8, (4) (2000) 393 - 450

    Article  MathSciNet  MATH  Google Scholar 

  34. Grädel, E.: On the restraining power of guards. The Journal of Symbolic Logic, 64 (1999) 1719 - 1742

    Article  MathSciNet  MATH  Google Scholar 

  35. Halmos, P.: Algebraic logic I. Monadic Boolean algebras. Compositio Mathematica, 12 (1955) 217 - 249

    MathSciNet  Google Scholar 

  36. Hartonas, C.: Duality for lattice-ordered algebras and for normal algebraizable logics. Studia Logica, 58, (3) (1997) 403 - 450

    Article  MathSciNet  MATH  Google Scholar 

  37. Hartonas, C. and Dunn, J.M.: Stone duality for lattices. Algebra Universalis, 37, (3) (1997) 391 - 401

    Article  MathSciNet  MATH  Google Scholar 

  38. Hâjek, P.: Metamathematics of Fuzzy Logic. Trends in Logic, Volume 4. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  39. Isandi, K. and Tanaka, S.: Ideal theory of BCK-algebras. Mathematica Japonica, 21 (1976) 351 - 366

    MathSciNet  Google Scholar 

  40. Iturrioz, L.: A topological representation theory for orthomodular lattices. In Colloquia Mathematica Societatis Janos Bolyai, volume 33. Contributions to Lattice Theory (1980) 503 - 524

    Google Scholar 

  41. Iturrioz, L.: Symmetrical Heyting algebras with operators. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 29 (1983) 33 - 70

    Article  MathSciNet  MATH  Google Scholar 

  42. Iturrioz, L. and Orlowska, E.: A Kripke-style and relational semantics for logics based on Lukasiewicz algebras. Conference in honour of J. Lukasiewicz, Dublin (1996)

    Google Scholar 

  43. Jônsson, B. and Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics, 73 (1951) 891 - 939

    Article  MathSciNet  MATH  Google Scholar 

  44. Jônsson, B. and Tarski, A.: Boolean algebras with operators, Part II. Americal Journal of Mathematics, 74 (1952) 127 - 162

    Article  MATH  Google Scholar 

  45. Lambek, J.: The mathematics of sentence structure. American Mathematical Monthly, 65 (1958) 154 - 170

    Article  MathSciNet  MATH  Google Scholar 

  46. Lambek, J.: On the calculus of syntactic types. In Jacobsen, R. editor, Structure of Language and its Mathematical Aspects, Proceedings of Symposia in Applied Mathematics, XII. American Mathematical Society (1961)

    Google Scholar 

  47. Representation Theorems 99

    Google Scholar 

  48. Lukasiewicz, J.: Philosophische Bemerkungen zu mehrwertigen Systemen des Aussagenkalküls. Comptes rendus de la Société des Sciences et Lettres de Varsovie, cl.iii, 23 (1930) 51-77. English translation in [47].

    Google Scholar 

  49. Lukasiewicz, J.: Selected works (ed. by L. Borkowski ). North-Holland (1970)

    Google Scholar 

  50. MacCaull, W.: Kripke semantics for logics with BCK implication. Bulletin of the Section of Logic of the University of Lodz, 25, (1) (1996) 41 - 51

    MathSciNet  MATH  Google Scholar 

  51. MacCaull, W.: A note on a Kripke semantics for residuated logic. Fuzzy sets and systems, 77 (1996) 229 - 234

    Article  MathSciNet  MATH  Google Scholar 

  52. Martinez, N.G.: A topological duality for some ordered lattice ordered algebraic structures including l-groups. Algebra Universalis, 31 (1994) 516 - 541

    Article  MathSciNet  MATH  Google Scholar 

  53. Meredith, C.A. and Prior, A.N.: Notes on the axiomatics of the propositional calculus. Notre Dame Journal of Formal Logic, 4 (1963) 171 - 187

    Article  MathSciNet  MATH  Google Scholar 

  54. Mortimer, M.: On languages with two variables. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 21 (1975) 135 - 140

    Article  MathSciNet  MATH  Google Scholar 

  55. Ohlbach, H.J.: Translation methods for non-classical logics: An overview. Bulletin of the IGPL, 1, (1) (1993) 69 - 89

    Article  MathSciNet  MATH  Google Scholar 

  56. Ono, H.: Algebraic aspects of logics without structural rules. AMS, Contemporary Mathematics, 131 part 3 (1992) 601 - 621

    Article  Google Scholar 

  57. Ono, H.: Semantics for substructural logics. In Schroeder-Heister, P. and Dosen, K. editors, Substructural Logics. Oxford University Press (1993) 259 - 291

    Google Scholar 

  58. Ono, H. and Komori, Y.: Logics without the contraction rule. Journal of Symbolic Logic, 50 (1985) 169 - 201

    Article  MathSciNet  MATH  Google Scholar 

  59. Orlowska, E.: Personal communication (1999)

    Google Scholar 

  60. Palasinski, M.: An embedding theorem for BCK-algebras. Math. Seminar Notes Kobe Univ., 10 (1982) 749 - 751

    Google Scholar 

  61. Priestley, H.A.: Representation of distributive lattices by means of ordered Stone spaces. Bulletin of the London Mathematical Society, 2 (1970) 186 - 190

    Article  MathSciNet  MATH  Google Scholar 

  62. Rodriguez, A.J.: Un estudo algebraico de los câlculos proposicionales de Lukasiewicz. PhD thesis, Universidad de Barcelona (1980)

    Google Scholar 

  63. Routley, R., Plumwood, R.V., Meyer, K. and Brady, R.T.: Relevant Logics and their Rivals. Ridgeview (1982)

    MATH  Google Scholar 

  64. Schmidt, R.: Optimized modal translation and resolution. PhD thesis, MaxPlanck-Institut für Informatik, Universität des Saarlandes (1997)

    Google Scholar 

  65. Schmidt, R.: Decidability by resolution for propositional modal logics. Journal of Automated Reasoning, 22, (4) (1999) 379 - 396

    Article  MathSciNet  MATH  Google Scholar 

  66. Sofronie-Stokkermans, V.: Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems. PhD thesis, RISC-Linz, J.Kepler University Linz, Austria (1997)

    Google Scholar 

  67. Sofronie-Stokkermans, V.: On the universal theory of varieties of distributive lattices with operators: Some decidability and complexity results. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, Trento, Italy, Springer (1999) 157 - 171

    Google Scholar 

  68. Sofronie-Stokkermans, V.: Representation theorems and automated theorem proving in non-classical logics. In Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, Freiburg im Breisgau, Germany. IEEE Computer Society, IEEE Computer Society Press (1999) 242 - 247

    Google Scholar 

  69. Viorica Sofronie-Stokkermans

    Google Scholar 

  70. Sofronie-Stokkermans, V.: Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of nonclassical logics I. Studia Logica, 64, (1) (2000) 93 - 132

    Article  MathSciNet  MATH  Google Scholar 

  71. Sofronie-Stokkermans, V.: Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of nonclassical logics II. Studia Logica, 64, (2) (2000) 151 - 172

    Article  MathSciNet  MATH  Google Scholar 

  72. Sofronie-Stokkermans, V.: Priestley duality for SHn-algebras and applications to the study of Kripke-style models for SHn-logics. Multiple-Valued Logic - An International Journal, 5, (4) (2000) 281 - 305

    MathSciNet  MATH  Google Scholar 

  73. Sofronie-Stokkermans, V.: Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators. Multiple-Valued Logic - An International Journal, 6 (2001) 289 - 344

    MathSciNet  MATH  Google Scholar 

  74. Sofronie-Stokkermans, V.: Representation theorems for distributive lattices with operators. Manuscript (2001)

    Google Scholar 

  75. Sofronie-Stokkermans, V.: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators. Research Report MPI-I-2001-2-005, Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany, September (2001)

    Google Scholar 

  76. Stone, M.H.: The theory of representations for Boolean algebras. Transactions of the American Mathematical Society (1936)

    Google Scholar 

  77. Szwast, W. and Tendera, L.: On the decision problem for the guarded fragment with transitivity. In Proceedings of the 16th IEEE Annual Symposium on Logic in Computer Science. IEEE Computer Society (2001) 147 - 156

    Google Scholar 

  78. Tarski, A.: Uber die Erweiterung der unvollständigen Systeme des Aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums, 7 (1934/1935) 51-57. English Translation in [76].

    Google Scholar 

  79. Tarski, A.: Logic, Semantics, Metamathematics: Papers from 1923 to 1938, ( Woodger, J.H. editor). Clarendon Press, Oxford (1956)

    Google Scholar 

  80. Urquhart, A.: A topological representation theory for lattices. Algebra Universalis, 8 (1978) 45 - 58

    Article  MathSciNet  MATH  Google Scholar 

  81. Urquhart, A.: Duality for algebras of relevant logics. Studia Logica, 56, (1,2) (1996) 263 - 276

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Authors
  1. Viorica Sofronie-Stokkermans
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics and Computer Science, Lehmann College, 250 Bedford Park Boulevard West, 10468-1589, Bronx, NY, USA

    Melvin Fitting

  2. National Institute of Telecommunications, ul. Szachowa 1, 04-894, Warsaw, Poland

    Ewa Orłowska

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Sofronie-Stokkermans, V. (2003). Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving. In: Fitting, M., Orłowska, E. (eds) Beyond Two: Theory and Applications of Multiple-Valued Logic. Studies in Fuzziness and Soft Computing, vol 114. Physica, Heidelberg. https://doi.org/10.1007/978-3-7908-1769-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-7908-1769-0_3

  • Publisher Name: Physica, Heidelberg

  • Print ISBN: 978-3-7908-2522-0

  • Online ISBN: 978-3-7908-1769-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation