Sequent of Relations Calculi: A Framework for Analytic Deduction in Many-valued Logics

  • Matthias Baaz
  • Agata Ciabattoni
  • Christian G. Fermüller
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


We present a general framework that allows to construct systematically analytic calculi for a large family of (propositional) many-valued logics — called projective logics — characterized by a special format of their semantics. All finite-valued logics as well as infinite-valued Gödel logic are projective. As a case-study, sequent of relations calculi for Gödel logics are derived. A comparison with some other analytic calculi is provided.


Semantic Theory Atomic Formula Propositional Variable Structural Rule Sequent Calculus 
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.
    Avellone, A., Ferrari, M. and Miglioli, P.: Duplication-free tableau calculi together with cut-free and contraction free sequent calculi for the interpolable propositional intermediate logics. Logic J. of the IGPL, 7, (4) (1999) 447–480MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    Avron, A.: Hypersequents, logical consequence and intermediate logics for con-currency. Annals of Mathematics and Artificial Intelligence, 4 (1991) 225–248MathSciNetMATHCrossRefGoogle Scholar
  3. 3.
    Avron, A.: The method of hypersequents in the proof theory of propositional nonclassical logics. In Logic: from Foundations to Applications, European Logic Colloquium. Oxford Science Publications. Clarendon Press. Oxford (1996) 1–32Google Scholar
  4. 4.
    Avron, A.: A tableau system for Gödel-Dummett logic based on a hypersequential calculus. In Automated Reasoning with Tableaux and Related Methods (Tableaux’2000), volume 1847 of Lectures Notes in Artificial Intelligence (2000) 98–112Google Scholar
  5. 5.
    Avron, A. and Konikowska, B.: Decomposition proof systems for Gödel logics. Studia Logica, 69 (2001) 197–219MathSciNetMATHCrossRefGoogle Scholar
  6. 6.
    Baaz, M.: Infinite-valued Gödel logics with 0–1-projections and relativizations. In Gödel 96. Kurt Gödel’s Legacy, volume 6 of LNL (1996) 23–33Google Scholar
  7. 7.
    Baaz, M., Ciabattoni, A. and Fermüller, C.: Cut-elimination in a sequentsof-relations calculus for Gödel logic. In International Symposium on Multiple Valued Logic (ISMVL’2001). IEEE (2001) 181–186Google Scholar
  8. 8.
    Baaz, M. and Fermliller, C.: Analytic calculi for projective logics. In Automated Reasoning with Tableaux and Related Methods (Tableaux’99), volume 1617 of Lectures Notes in Artificial Intelligence (1999) 36–51Google Scholar
  9. 9.
    Baaz, M., Fermüller, C. and Salzer, G.: Automated deduction for many-valued logic. In Handbook of Automated Reasoning. Elsevier (2001)Google Scholar
  10. 10.
    Baaz, M., Fermüller, C. and Zach, R • Elimination of cuts in first-order finite-valued logics. J. Inform. Process. Cybernet. EIK, 29, (6) (1994) 333–355Google Scholar
  11. 11.
    Bachmair, L. and Ganzinger, H.: Ordered chaining for total orderings. In CADE`94, volume 814 of Lecture Notes in Computer Science (1994) 435–450Google Scholar
  12. 12.
    Bachmair, L. and Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. of the ACM, 45, (6) (1998) 1007–1049MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Ciabattoni, A. and Ferrari, M.: Hypersequent calculi for some intermediate logics with bounded Kripke models. J. of Logic and Computation, 2, (11) (2001) 283–294MathSciNetCrossRefGoogle Scholar
  14. 14.
    Dummett, M.: A propositional logic with denumerable matrix. J. of Symbolic Logic, 24 (1959) 96–107MathSciNetGoogle Scholar
  15. 15.
    Dunn, J.M. and Meyer, R.K.: Algebraic completeness results for Dummett’s LC and its extensions. Z. Math. Logik Grundlagen Math, 17 (1971) 225–230MathSciNetMATHCrossRefGoogle Scholar
  16. 16.
    Dyckhoff, R.: A deterministic terminating sequent calculus for Gödel Dummett logic. Logic Journal of the IGPL, 7 (1999) 319–326MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Gentzen, G.: Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift, 39 (1934) and (1935) 176–210 and 405–431Google Scholar
  18. 18.
    Gödel, K.: Zum intuitionistischen Aussagenkalkül. Anz. Akad. Wiss. Wien, 69 (1932) 65–66MATHGoogle Scholar
  19. 19.
    Hâjek, P.: Metamathematics of Fuzzy Logic. Kluwer (1998)Google Scholar
  20. 20.
    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
  21. 21.
    Lukasiewicz, J.: Philosophische Bemerkungen zu mehrwertigen Systemen der Aussagenlogik. Comptes Rendus de la Societé des Science et de Lettres de Varsovie (1930) 51–77Google Scholar
  22. 22.
    Moisil, G.: Essais sur les logiques non chrysipiennes. Editions de l’Academie de la Republique Socialiste de Roumanie, Bucarest (1972)Google Scholar
  23. 23.
    Rousseau, G.: Sequents in many valued logic I. Fund. Math., 60 (1967) 23–33MathSciNetGoogle Scholar
  24. 24.
    Schütte, K.: Proof Theory. Springer, Berlin and New York (1977)MATHCrossRefGoogle Scholar
  25. 25.
    Sonobe, O.: A Gentzen-type formulation of some intermediate propositional logics. J. of Tsuda College, 7 (1975) 7–14MathSciNetGoogle Scholar
  26. 26.
    Takahashi, M.: Many-valued logics of extended Gentzen style I. Science Reports of the Tokyo Kyoiku Daigaku, 9 (1967) 95–116Google Scholar
  27. 27.
    Takeuti, G. and Titani, T.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. of Symbolic Logic, 49 (1984) 851–866MathSciNetMATHCrossRefGoogle Scholar
  28. 28.
    Troelstra, A.S. and Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (1996)Google Scholar
  29. 29.
    Visser, A.: On the completeness principle: a study of provability in Heyting’s Arithmetic. Annals of Math. Logic, 22 (1982) 263–295MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Matthias Baaz
    • 1
  • Agata Ciabattoni
    • 1
  • Christian G. Fermüller
    • 1
  1. 1.Technische Universität WienViennaAustria

Personalised recommendations