Abstract
We present a terminating contraction-free calculus GLC * for the propositional fragment of Gödel-Dummett Logic LC. GLC * uses hypersequents, and unlike other Gentzen-type calculi for LC, all its rules have at most two premises. These rules are all invertible. Hence it can be used as a basis for a deterministic tableau system for LC. This tableau system is presented in the last section.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avellone, A., Ferrari, M., Miglioli, P.: Duplication-free Tableaux Calculi Together with Cut-free and Contraction-free Sequent Calculi for the Interpolable Propositional Intermediate Logics. Logic J. IGPL 7, 447–480 (1999)
Avron, A.: Using Hypersequents in Proof Systems for Non-classical Logics. Annals of Mathematics and Artificial Intelligence 4, 225–248 (1991)
Baaz, M., Fermüller, G.C.: Analytic Calculi for Projective Logics. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 36–50. Springer, Heidelberg (1999)
Dunn, J.M., Meyer, R.K.: Algebraic Completeness Results for Dummett’s LC and its extensions. Z. math. Logik und Grundlagen der Mathematik 17, 225–230 (1971)
Dummett, M.: A Propositional Calculus with a Denumerable matrix. Journal of Symbolic Logic 24, 96–107 (1959)
Dyckhoff, R.: A Deterministic Terminating Sequent Calculus for Gödel-Dummett Logic. Logic J. IGPL 7, 319–326 (1999)
Gödel, K.: Zum intuitionistischen Aussagenkalkül, Ergeb. Math. Koll. 4, 40 (1933)
Hajek, P.: Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, Dordrecht (1998)
Sonobe, O.: A Gentzen-type Formulation of Some Intermediate Propositional Logics. Journal of Tsuda College 7, 7–14 (1975)
Visser, A.: On the Completeness Principle: A study of provability in Heyting’s arithmetic. Annals of Mathematical Logic 22, 263–295 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avron, A. (2000). A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus. In: Dyckhoff, R. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000. Lecture Notes in Computer Science(), vol 1847. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722086_11
Download citation
DOI: https://doi.org/10.1007/10722086_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67697-3
Online ISBN: 978-3-540-45008-5
eBook Packages: Springer Book Archive