Abstract
The class of projective propositional logics is defined by a certain format of the definition of truth functions for their connectives with respect to a semantic theory. All finite valued logics, but also infinite valued Gödel logic are shown to be projective. Analytic Gentzen type calculi are uniformly derived for all projective logics. Admissibility of cut rules and other structural rules is investigated. The special case of Gödel logics is exemplified in detail and compared with the previous approach of Avron (based on hypersequents).
Partly supported by COST-Action No. 15 and FWF grant P-12652-MAT.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Kurt Schütte. Proof Theory. Springer, Berlin and New York, 1977.
Nicholas Rescher. Many-valued Logic. McGraw-Hill, New York, 1969.
Petr Hajek. Metamathematics of Fuzzy Logic. Kluwer, 1998.
G. Rousseau. Sequents in many valued logic I. Fundamenta Mathematicae, 60:23–33, 1967.
Kurt Gödel. Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, 69:65–66, 1932.
Reiner Hähnle. Automated Deduction in Multiple-valued Logics. Clarendon Press, Oxford, 1993.
Michael Dummett. A propositional logic with denumerable matrix. Journal of Symbolic Logic, 24:96–107, 1959.
Moto-o Takahashi. Many-valued logics of extended Gentzen style I. Sci. Rep. Tokyo Kyoiku Daigaku Sect. A, 9(271):95–110, 1968.
Gerhard Gentzen. Untersuchungen über das logische Schließen I–II. Mathematische Zeitschrift, 39:176–210 and 405–431, 1934–35.
Hans Jürgen Ohlbach. Computer support for the development and investigation of logics. Technical Report MPI-I-94-228, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1994.
Arnon Avron. Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence, 4(199):225–248, 1991.
Matthias Baaz and Christian G. Fermüller. Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computation, 19:353–391, 1995.
Arnon Avron. The method of hypersequents in proof theory of propositional nonclassical logics. In Logic: from foundations to applications. European logic colloquium, Keele, UK, July 20–29, 1993, pages 1–32, Oxford, 1996. Clarendon Press.
Matthias Baaz, Gernot Salzer, Christian G. Fermüller, and Richard Zach. MUlt-log 1.0: Towards an expert system for many-valued logics. In 13th Int. Conf. on Automated Deduction (CADE’96), volume 1104 of Lecture Notes in Artificial Intelligence, pages 226–230. Springer, 1996.
Matthias Baaz, Christian G. Fermüller, and Richard Zach. Elimination of cuts in first-order finite-valued logics. J. Inform. Process. Cybernet. EIK, 29(6):333–355, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baaz, M., Fermüller, C.G. (1999). Analytic Calculi for Projective Logics. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_8
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive