Complexity of Many-valued Logics

  • Reiner Hähnle
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


As is the case for other logics, a number of complexity-related questions can be posed in the context of many-valued logic. Some of these, such as the complexity of the sets of satisfiable and valid formulas in various logics, are completely standard; others only make sense in a many-valued context. In this overview I concentrate on two kinds of complexity problems related to many-valued logic: first, I discuss the complexity of the membership problem in various languages, such as the satisfiable, respectively, the valid formulas in some well-known logics. Second, I discuss the size of representations of many-valued connectives and quantifiers, because this has a direct impact on the complexity of many kinds of deduction systems. I include results on both propositional and on first-order logic.


Classical Logic Conjunctive Normal Form Disjunctive Normal Form Conjunctive Normal Form Formula Horn Formula 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aguzzoli, S.: The complexity of McNaughton functions of one variable. Advances in Applied Mathematics, 21, (1) (1998) 58–77MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    Aguzzoli, S.: Geometric and Proof Theoretic Issues in Lukasiewicz Propositional Logics. PhD thesis, University of Siena, Italy, Feb. (1999)Google Scholar
  3. 3.
    Aguzzoli, S. and Ciabattoni, A.: Finiteness in infinite-valued logic. Journal of Logic, Language and Information, 9, (1) (2000) 5–29MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Ausiello, G. and Giaccio, R.: On-line algorithms for satisfiability problems with uncertainty. Theoretical Computer Science, 171 (1–2) Jan. (1997) 3–24Google Scholar
  5. 5.
    Baaz, M. and Fermüller, C.G.: Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computation, 19, (4) Apr. (1995) 353–391Google Scholar
  6. 6.
    Baaz, M., Fermüller, C.G., Salzer, G. and Zach, R.: Labeled calculi and finite-valued logics. Studia Logica, 61, (1) (1998) 7–33MathSciNetMATHCrossRefGoogle Scholar
  7. 7.
    Baaz, M., Hâjek, P., Montagna, F. and Veith, H.: Complexity of t-tautologies. Annals of Pure and Applied Logic, to appear (2001)Google Scholar
  8. 8.
    Baaz, M., Hâjek, P., Svejda, D. and Krajfcek, J.: Embedding logics into product logic. Studia Logica, 61, (1), July (1998) 35–47Google Scholar
  9. 9.
    Baaz, M., Leitsch, A. and Zach, R.: Incompleteness of a first-order Gödel logic and some temporal logics of programs. In Kleine Büning, H. editor, Selected Papers from Computer Science Logic, CSL’95, Paderborn, Germany, volume 1092 of LNCS. Springer-Verlag (1996) 1–15Google Scholar
  10. 10.
    Beckert, B., Hähnle, R. and Manyä, F.: Transformations between signed and classical clause logic. In Proc. 29th International Symposium on Multiple-Valued Logics, Freiburg, Germany. IEEE CS Press, Los Alamitos, May (1999) 248–255Google Scholar
  11. 11.
    Beckert, B., Hähnle, R. and Manyä, F.: The 2-SAT problem of regular signed CNF formulas. In Proc. 30th International Symposium on Multiple-Valued Logics, Portland/OR, USA. IEEE CS Press, Los Alamitos, May (2000) 331–336Google Scholar
  12. 12.
    Beckert, B., Hähnle, R. and Manyä, F.: The SAT problem of signed CNF formulas. In Basin, D., D’Agostino, M., Gabbay, D., Matthews, S. and Viganô, L. editors, Labelled Deduction, volume 17 of Applied Logic Series. Kluwer, Dordrecht, May (2000) 61–82Google Scholar
  13. 13.
    Béjar, R.: Systematic and Local Search Algorithms for Regular-SAT. PhD thesis, Facultat de Ciències, Universitat Autônoma de Barcelona (2000)Google Scholar
  14. 14.
    Béjar, R., Hähnle, R. and Manyä, F.: A modular reduction of regular logic to classical logic. In Proc. 31st International Symposium on Multiple-Valued Logics, Warsaw, Poland. IEEE CS Press, Los Alamitos, May (2001) 221–226CrossRefGoogle Scholar
  15. 15.
    Béjar, R. and Manyà, F.: Phase transitions in the regular random 3-SAT problem. In Z. W. Rag and A. Skowron, editors, Proc. International Symposium on Methodologies for Intelligent Systems, ISMIS’99, Warsaw, Poland, number 1609 in LNCS. Springer-Verlag (1999) 292–300Google Scholar
  16. 16.
    Burch, J., Clarke, E., McMillan, K. and Dill, D.: Sequential circuit verification using symbolic model checking. In Proc. 27th ACM/IEEE Design Automation Conference ( DAC ). ACM Press, (1990) 46–51CrossRefGoogle Scholar
  17. 17.
    Cadoli, M. and Schaerf, M.: On the complexity of entailment in propositional multivalued logics. Annals of Mathematics and Artificial Intelligence, 18, (1) (1996) 29–50MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
    Carnielli, W.A.: On sequents and tableaux for many-valued logics. Journal of Non-Classical Logic, 8, (1), May (1991) 59–76Google Scholar
  19. 19.
    Ciabattoni, A.: Proof Theoretic Techniques in Many-Valued Logics. PhD thesis, University of Milan, Italy, Jan. (2000)Google Scholar
  20. 20.
    Cignoli, R.L.O., D’Ottaviano, I.M.L. and Mundici, D.: Algebraic Foundations of Many-Valued Reasoning, volume 7 of Trends in Logic. Kluwer, Dordrecht, Nov. (1999)Google Scholar
  21. 21.
    Clarke, E.M., Grumberg, O. and Peled, D.A.: Model Checking. The MIT Press, Cambridge, Massachusetts (1999)Google Scholar
  22. 22.
    Dowling, W. and Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 3 (1984) 267284Google Scholar
  23. 23.
    Dueck, G.W. and Butler, J.T.: Multiple-valued logic operations with universal literals. In Proc. 24th International Symposium on Multiple-Valued Logic, Boston/MA. IEEE CS Press, Los Alamitos, May (1994) 73–79Google Scholar
  24. 24.
    Escalada-Imaz, G. and Manyà, F.: The satisfiability problem for multiple-valued Horn formule. In Proc. International Symposium on Multiple-Valued Logics, ISMVL’94, Boston/MA, USA. IEEE CS Press, Los Alamitos (1994) 250–256Google Scholar
  25. 25.
    Even, S., Itai, A. and Shamir, A.: On the complexity of timetable and multi-commodity flow problems. SIAM Journal of Computing, 5, (4) (1976) 691–703MathSciNetMATHCrossRefGoogle Scholar
  26. 26.
    Gödel, K.: Zum intuitionistischen Aussagenkalkül. Anzeiger Akademie der Wissenschaften Wien, mathematisch-naturwiss. Klasse, 32 (1932) 65–66. Reprinted and translated in [27].Google Scholar
  27. 27.
    Gödel, K.: Collected Works: Publications 1929–1936, volume 1. Oxford University Press (1986). Edited by Solomon Feferman, John Dawson, and Stephen Kleene.MATHGoogle Scholar
  28. 28.
    Gottwald, S.: A Treatise on Many-Valued Logics, volume 9 of Studies in Logic and Computation. Research Studies Press, Baldock, Nov. (2000)Google Scholar
  29. 29.
    Hähnle, R.: Automated Deduction in Multiple-Valued Logics, volume 10 of International Series of Monographs on Computer Science. Oxford University Press (1994)Google Scholar
  30. 30.
    Hähnle, R.: Many-valued logic and mixed integer programming. Annals of Mathematics and Artificial Intelligence, 12, (3,4), Dec. (1994) 231–264Google Scholar
  31. 31.
    Hähnle, R.: Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4, (6) (1994) 905–927MathSciNetMATHCrossRefGoogle Scholar
  32. 32.
    Hähnle, R.: Exploiting data dependencies in many-valued logics. Journal of Applied Non-Classical Logics, 6, (1) (1996) 49–69MathSciNetMATHCrossRefGoogle Scholar
  33. 33.
    Hähnle, R.: Proof theory of many-valued logic—linear optimization—logic design: Connections and interactions. Soft Computing—A Fusion of Foundations, Methodologies and Applications, 1, (3), Sept. (1997) 107–119Google Scholar
  34. 34.
    Hähnle, R.: Commodious axiomatization of quantifiers in multiple-valued logic. Studia Logica, Special Issue on Many-Valued Logics, their Proof Theory and Algebras, 61, (1) (1998) 101–121.MATHGoogle Scholar
  35. 35.
    Hähnle, R.: Tableaux for many-valued logics. In D’Agostino, M., Gabbay, D., Hähnle, R. and Posegga, J. editors, Handbook of Tableau Methods. Kluwer, Dordrecht (1999) 529–580CrossRefGoogle Scholar
  36. 36.
    Hähnle, R.: Advanced many-valued logics. In Gabbay, D.M. and Guenthner, F. editors, Handbook of Philosophical Logic, volume 2. Kluwer, Dordrecht, 2nd edition, Aug. (2001) 297–395Google Scholar
  37. 37.
    Hähnle, R.: Complexity of many-valued logics. In Proc. 31st International Symposium on Multiple-Valued Logics, Warsaw, Poland. Invited Tutorial. IEEE CS Press, Los Alamitos, May (2001) 137–146CrossRefGoogle Scholar
  38. 38.
    Hâjek, P.: Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic: Studia Logica Library. Kluwer Academic Publishers, Dordrecht (1998)CrossRefGoogle Scholar
  39. 39.
    Hâjek, P., Godo, L. and Esteva, F.: A complete many-valued logic with product conjunction. Archive for Mathematical Logic, 35 (1996) 191–208MathSciNetMATHGoogle Scholar
  40. 40.
    Hâjek, P. and Tulipani, S.: Complexity of fuzzy probability logics. Fundamenta Informaticœ, 45, (3) (2001) 207–213MATHGoogle Scholar
  41. 41.
    Hooker, J.N.: A quantitative approach to logical inference. Decision Support Systems, 4 (1988) 45–69CrossRefGoogle Scholar
  42. 42.
    Jeroslow, R.G.: Logic-Based Decision Support. Mixed Integer Model Formulation. Elsevier, Amsterdam (1988)Google Scholar
  43. 43.
    Kirin, V.G.: Gentzen’s method of the many-valued propositional calculi. Zeitschrift für mathematische Logik and Grundlagen der Mathematik, 12 (1966) 317–332MathSciNetMATHCrossRefGoogle Scholar
  44. 44.
    Lukasiewicz, J.: Jan Lukasiewicz, Selected Writings. Edited by L. Borowski. North-Holland (1970)Google Scholar
  45. 45.
    Lukasiewicz, J. and Tarski, A.: Untersuchungen über den Aussagenkalkül. Comptes Rendus des Séances de la Societé des Sciences et des Lettres de Varsovie, Classe III, 23 (1930) 1–21. Reprinted and translated in [44].Google Scholar
  46. 46.
    Manyà, F.: Proof Procedures for Multiple-Valued Propositional Logics. PhD thesis, Facultat de Ciències, Universitat Autbnoma de Barcelona (1996). Published as [47]Google Scholar
  47. 47.
    Manyà, F.: Proof Procedures for Multiple-Valued Propositional Logics, volume 9 of Monografies de l’Institut d’Investigacid en Intel•ligència Artificial. IIIA-CSIC, Bellaterra (Barcelona ) (1999)Google Scholar
  48. 48.
    Manyà, F.: The 2-SAT problem in signed CNF formulas. Multiple-Valued Logic. An International Journal, 5 (2000)Google Scholar
  49. 49.
    Manyà, F., Béjar, R. and Escalada-Imaz, G.: The satisfiability problem in regular CNF-formulas. Soft Computing—A Fusion of Foundations, Methodologies and Applications, 2, (3), Sept. (1998) 116–123Google Scholar
  50. 50.
    McNaughton, R.: A theorem about infinite-valued sentential logic. Journal of Symbolic Logic, 16, (1) (1951) 1–13MathSciNetMATHCrossRefGoogle Scholar
  51. 51.
    Mitchell, D., Selman, B. and Levesque, H.: Hard and easy distributions of SAT problems. In Proc. of AAAI-92, San Jose, CA (1992) 459–465Google Scholar
  52. 52.
    Mostowski, A.: Proofs of non-deducibility in intuitionistic functional calculus. Journal of Symbolic Logic, 13, (4), Dec. (1948) 204–207Google Scholar
  53. 53.
    Mundici, D.: Satisfiability in many-valued sentential logic is NP-complete. Theoretical Computer Science, 52 (1987) 145–153MathSciNetMATHCrossRefGoogle Scholar
  54. 54.
    Mundici, D.: A constructive proof of McNaughton’s Theorem in infinite-valued logic. Journal of Symbolic Logic, 59, (2), June (1994) 596–602Google Scholar
  55. 55.
    Mundici, D. and Olivetti, N.: Resolution and model building in the infinite-valued calculus of Lukasiewicz. Theoretical Computer Science, 200, (1–2) (1998) 335–366MathSciNetMATHCrossRefGoogle Scholar
  56. 56.
    Patel-Schneider, P. F.: A decidable first-order logic for knowledge representation. Journal of Automated Reasoning, 6 (1990) 361–388MathSciNetMATHCrossRefGoogle Scholar
  57. 57.
    Pogorzelski, W.A.: The deduction theorem for Lukasiewicz many-valued propositional calculi. Studia Logica, 15 (1964) 7–23MathSciNetMATHCrossRefGoogle Scholar
  58. 58.
    Ragaz, M.E.: Arithmetische Klassifikation von Formelmengen der unendlichwertigen Logik. PhD thesis, ETH Zürich (1981)MATHGoogle Scholar
  59. 59.
    Rosser, J.B. and Turquette, A.R.: Many-Valued Logics. North-Holland, Amsterdam (1952)MATHGoogle Scholar
  60. 60.
    Rousseau, G.: Sequents in many valued logic I. Fundamenta Mathematicœ, LX (1967) 23–33Google Scholar
  61. 61.
    Sasao, T.: Multiple-valued decomposition of generalized Boolean functions and the complexity of programmable logic arrays. IEEE Transactions on Computers, C-30, Sept. (1981) 635–643Google Scholar
  62. 62.
    Sasao, T.: Logic synthesis with EXOR gates. In Sasao, T. editor, Logic Synthesis and Optimization, chapter 12. Kluwer, Norwell/MA, USA (1993) 259–286CrossRefGoogle Scholar
  63. 63.
    Sasao, T.: Switching Theory for Logic Synthesis. Kluwer, Norwell/MA, USA (1999)Google Scholar
  64. 64.
    Sasao, T. and Butler, J.T.: Comparison of the worst and best sum-of-products expressions for multiple-valued functions. In Proc. 27th International Symposium on Multiple-Valued Logic, Nova Scotia, Canada. IEEE CS Press, Los Alamitos, May (1997) 55–60Google Scholar
  65. 65.
    Scarpellini, B.: Die Nichtaxiomatisierbarkeit des unendlichwertigen Prädikatenkalküls von Lukasiewicz. Journal of Symbolic Logic, 27, (2), June (1962) 159–170Google Scholar
  66. 66.
    Sistla, A. and Clarke, E.: The complexity of propositional linear temporal logics. Journal of the ACM, 32, (3) (1985) 733–749MathSciNetMATHCrossRefGoogle Scholar
  67. 67.
    Sofronie-Stokkermans, V.: On translation of finitely-valued logics to classical first-order logic. In Prade, H. editor, Proc. 13th European Conference on Artificial Intelligence, Brighton. John Wiley & Sons (1998) 410–411Google Scholar
  68. 68.
    Sofronie-Stokkermans, V.: Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators. Multiple-Valued Logic, 6, (3–4) (2001) 289–344MathSciNetMATHGoogle Scholar
  69. 69.
    Wagner, H.: Nonaxiomatizability and undecidability of an infinite-valued temporal logic. Multiple-Valued Logic, 2, (1) (1997) 47–58Google Scholar
  70. 70.
    Zach, R.: Proof theory of finite-valued logics. Master’s thesis, Institut für Algebra and Diskrete Mathematik, TU Wien, Sept. (1993). Also Technical Report TUW-E185.2-Z.1–93.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Reiner Hähnle
    • 1
  1. 1.Dept. of Computing ScienceChalmers University of TechnologyGothenburgSweden

Personalised recommendations