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

  • Viorica Sofronie-Stokkermans
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


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.


Modal Logic Distributive Lattice Representation Theorem Residuated Lattice Algebraic Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Anderson, A.R. and Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, volume 1. Princeton University Press, Princeton (1975)MATHGoogle Scholar
  2. 2.
    Allwein, G. and Dunn, J.M.: Kripke models for linear logic. Journal of Symbolic Logic, 58, (2) (1993) 514 - 545MathSciNetMATHCrossRefGoogle Scholar
  3. 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 - 274MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Blok, W.J. and Ferreirim, I.M.A.: On the structure of hoops. Algebra Universalis, 43 (2000) 233 - 257MathSciNetMATHCrossRefGoogle Scholar
  5. 5.
    Blyth, T.S. and Varlet, J.C.: Ockham Algebras. Oxford Science Publications (1994)Google Scholar
  6. 6.
    Brink, C.: Multisets and the algebra of relevance logic. The Journal of Nonclassical logic, 5 (1988) 75 - 95MathSciNetGoogle Scholar
  7. 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. 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 - 111Google Scholar
  9. 9.
    Davey, B.A. and Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press (1990)Google Scholar
  10. 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 - 108Google Scholar
  11. 11.
    Dummet, M.: A propositional calculus with denumerable matrix. The Journal of Symbolic Logic, 24, (2) (1959) 97 - 106MathSciNetCrossRefGoogle Scholar
  12. 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 - 108Google Scholar
  13. 13.
    Dunn, J.M.: Positive modal logic. Studia Logica, 55 (1995) 301 - 317MathSciNetMATHCrossRefGoogle Scholar
  14. 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 - 100MATHCrossRefGoogle Scholar
  15. 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. 16.
    Fleischer, I.: Every BCK-algebra is a set of residuables in an integral pomonoid. Journal of Algebra, 119 (1988) 360 - 365MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Gabbay, D.: Expressive functional completeness in tense logics. In Mönnich, U. editor, Aspects of Philosophical Logic. Reidel (1981) 91 - 117Google Scholar
  18. 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 - 246Google Scholar
  19. 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 - 34Google Scholar
  20. 20.
    Gehrke, M.: Personal communication (2001)Google Scholar
  21. 21.
    Gehrke, M. and Priestley, H.A.: Non-canonicity of MV-algebras. Houston Journal of Mathematics. To appear.Google Scholar
  22. 98.
    Viorica Sofronie-StokkermansGoogle Scholar
  23. 22.
    Gehrke, M. and Harding, J.: Bounded lattice expansions. Journal of Algebra, 238 (2001) 345 - 371MathSciNetMATHCrossRefGoogle Scholar
  24. 23.
    Gehrke, M. and Jônsson, B.: Bounded distributive lattices with operators. Mathematica Japonica, 40, (2) (1994) 207 - 215MathSciNetMATHGoogle Scholar
  25. 24.
    Gehrke, M. and Jônsson, B.: Monotone bounded distributive lattice expansions. Mathematica Japonica, 52, (2) (2000) 197 - 213MathSciNetMATHGoogle Scholar
  26. 25.
    Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift (1935)Google Scholar
  27. 26.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science (1987)Google Scholar
  28. 27.
    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 - 69MathSciNetMATHCrossRefGoogle Scholar
  29. 28.
    Goldblatt, R.: Semantic analysis of orthologic. Journal of Philosophical Logic, 3 (1974) 19 - 35MathSciNetCrossRefGoogle Scholar
  30. 29.
    Goldblatt, R.: Orthomodularity is not elementary. The Journal of Symbolic Logic, 49 (1984) 401 - 404MathSciNetMATHCrossRefGoogle Scholar
  31. 30.
    Goldblatt, R.: Varieties of complex algebras. Annals of Pure and Applied Logic, 44, (3) (1989) 153 - 301MathSciNetCrossRefGoogle Scholar
  32. 31.
    Goldblatt, R.: Mathematics of modality, volume 43 of Center for the Study of Language and Information. Univ. of Chicago Press (1993)Google Scholar
  33. 32.
    Goldblatt, R.: Algebraic polymodal logic: A survey. Logic Journal of the IGPL, 8, (4) (2000) 393 - 450MathSciNetMATHCrossRefGoogle Scholar
  34. 33.
    Grädel, E.: On the restraining power of guards. The Journal of Symbolic Logic, 64 (1999) 1719 - 1742MathSciNetMATHCrossRefGoogle Scholar
  35. 34.
    Halmos, P.: Algebraic logic I. Monadic Boolean algebras. Compositio Mathematica, 12 (1955) 217 - 249MathSciNetGoogle Scholar
  36. 35.
    Hartonas, C.: Duality for lattice-ordered algebras and for normal algebraizable logics. Studia Logica, 58, (3) (1997) 403 - 450MathSciNetMATHCrossRefGoogle Scholar
  37. 36.
    Hartonas, C. and Dunn, J.M.: Stone duality for lattices. Algebra Universalis, 37, (3) (1997) 391 - 401MathSciNetMATHCrossRefGoogle Scholar
  38. 37.
    Hâjek, P.: Metamathematics of Fuzzy Logic. Trends in Logic, Volume 4. Kluwer Academic Publishers, Dordrecht (1998)Google Scholar
  39. 38.
    Isandi, K. and Tanaka, S.: Ideal theory of BCK-algebras. Mathematica Japonica, 21 (1976) 351 - 366MathSciNetGoogle Scholar
  40. 39.
    Iturrioz, L.: A topological representation theory for orthomodular lattices. In Colloquia Mathematica Societatis Janos Bolyai, volume 33. Contributions to Lattice Theory (1980) 503 - 524Google Scholar
  41. 40.
    Iturrioz, L.: Symmetrical Heyting algebras with operators. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 29 (1983) 33 - 70MathSciNetMATHCrossRefGoogle Scholar
  42. 41.
    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. 42.
    Jônsson, B. and Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics, 73 (1951) 891 - 939MathSciNetMATHCrossRefGoogle Scholar
  44. 43.
    Jônsson, B. and Tarski, A.: Boolean algebras with operators, Part II. Americal Journal of Mathematics, 74 (1952) 127 - 162MATHCrossRefGoogle Scholar
  45. 44.
    Lambek, J.: The mathematics of sentence structure. American Mathematical Monthly, 65 (1958) 154 - 170MathSciNetMATHCrossRefGoogle Scholar
  46. 45.
    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 99Google Scholar
  48. 46.
    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. 47.
    Lukasiewicz, J.: Selected works (ed. by L. Borkowski ). North-Holland (1970)Google Scholar
  50. 48.
    MacCaull, W.: Kripke semantics for logics with BCK implication. Bulletin of the Section of Logic of the University of Lodz, 25, (1) (1996) 41 - 51MathSciNetMATHGoogle Scholar
  51. 49.
    MacCaull, W.: A note on a Kripke semantics for residuated logic. Fuzzy sets and systems, 77 (1996) 229 - 234MathSciNetMATHCrossRefGoogle Scholar
  52. 50.
    Martinez, N.G.: A topological duality for some ordered lattice ordered algebraic structures including l-groups. Algebra Universalis, 31 (1994) 516 - 541MathSciNetMATHCrossRefGoogle Scholar
  53. 51.
    Meredith, C.A. and Prior, A.N.: Notes on the axiomatics of the propositional calculus. Notre Dame Journal of Formal Logic, 4 (1963) 171 - 187MathSciNetMATHCrossRefGoogle Scholar
  54. 52.
    Mortimer, M.: On languages with two variables. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 21 (1975) 135 - 140MathSciNetMATHCrossRefGoogle Scholar
  55. 53.
    Ohlbach, H.J.: Translation methods for non-classical logics: An overview. Bulletin of the IGPL, 1, (1) (1993) 69 - 89MathSciNetMATHCrossRefGoogle Scholar
  56. 54.
    Ono, H.: Algebraic aspects of logics without structural rules. AMS, Contemporary Mathematics, 131 part 3 (1992) 601 - 621CrossRefGoogle Scholar
  57. 55.
    Ono, H.: Semantics for substructural logics. In Schroeder-Heister, P. and Dosen, K. editors, Substructural Logics. Oxford University Press (1993) 259 - 291Google Scholar
  58. 56.
    Ono, H. and Komori, Y.: Logics without the contraction rule. Journal of Symbolic Logic, 50 (1985) 169 - 201MathSciNetMATHCrossRefGoogle Scholar
  59. 57.
    Orlowska, E.: Personal communication (1999)Google Scholar
  60. 58.
    Palasinski, M.: An embedding theorem for BCK-algebras. Math. Seminar Notes Kobe Univ., 10 (1982) 749 - 751Google Scholar
  61. 59.
    Priestley, H.A.: Representation of distributive lattices by means of ordered Stone spaces. Bulletin of the London Mathematical Society, 2 (1970) 186 - 190MathSciNetMATHCrossRefGoogle Scholar
  62. 60.
    Rodriguez, A.J.: Un estudo algebraico de los câlculos proposicionales de Lukasiewicz. PhD thesis, Universidad de Barcelona (1980)Google Scholar
  63. 61.
    Routley, R., Plumwood, R.V., Meyer, K. and Brady, R.T.: Relevant Logics and their Rivals. Ridgeview (1982)MATHGoogle Scholar
  64. 62.
    Schmidt, R.: Optimized modal translation and resolution. PhD thesis, MaxPlanck-Institut für Informatik, Universität des Saarlandes (1997)Google Scholar
  65. 63.
    Schmidt, R.: Decidability by resolution for propositional modal logics. Journal of Automated Reasoning, 22, (4) (1999) 379 - 396MathSciNetMATHCrossRefGoogle Scholar
  66. 64.
    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. 65.
    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 - 171Google Scholar
  68. 66.
    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 - 247Google Scholar
  69. 100.
    Viorica Sofronie-StokkermansGoogle Scholar
  70. 67.
    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 - 132MathSciNetMATHCrossRefGoogle Scholar
  71. 68.
    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 - 172MathSciNetMATHCrossRefGoogle Scholar
  72. 69.
    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 - 305MathSciNetMATHGoogle Scholar
  73. 70.
    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 - 344MathSciNetMATHGoogle Scholar
  74. 71.
    Sofronie-Stokkermans, V.: Representation theorems for distributive lattices with operators. Manuscript (2001)Google Scholar
  75. 72.
    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. 73.
    Stone, M.H.: The theory of representations for Boolean algebras. Transactions of the American Mathematical Society (1936)Google Scholar
  77. 74.
    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 - 156Google Scholar
  78. 75.
    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. 76.
    Tarski, A.: Logic, Semantics, Metamathematics: Papers from 1923 to 1938, ( Woodger, J.H. editor). Clarendon Press, Oxford (1956)Google Scholar
  80. 77.
    Urquhart, A.: A topological representation theory for lattices. Algebra Universalis, 8 (1978) 45 - 58MathSciNetMATHCrossRefGoogle Scholar
  81. 78.
    Urquhart, A.: Duality for algebras of relevant logics. Studia Logica, 56, (1,2) (1996) 263 - 276MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Viorica Sofronie-Stokkermans
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany

Personalised recommendations