nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents

verfasst von : Tim Lyon

Erschienen in: Logical Foundations of Computer Science

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper employs the linear nested sequent framework to design a new cut-free calculus (\(\mathsf {LNIF}\)) for intuitionistic fuzzy logic—the first-order Gödel logic characterized by linear relational frames with constant domains. Linear nested sequents—which are nested sequents restricted to linear structures—prove to be a well-suited proof-theoretic formalism for intuitionistic fuzzy logic. We show that the calculus \(\mathsf {LNIF}\) possesses highly desirable proof-theoretic properties such as invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Feedback Hyperjump

Nächstes Kapitel On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

We refer to [28] for a detailed discussion of fundamental proof-theoretic properties.

Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4(3), 225–248 (1991). https://doi.org/10.1007/BF01531058MathSciNetCrossRefMATH

Baaz, M., Ciabattoni, A., Preining, N.: SAT in monadic gödel logics: a borderline between decidability and undecidability. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS (LNAI), vol. 5514, pp. 113–123. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02261-6_10CrossRefMATH

Baaz, M., Preining, N., Zach, R.: First-order gödel logics. Ann. Pure Appl. Logic 147(1), 23–47 (2007). https://doi.org/10.1016/j.apal.2007.03.001. URL http://www.sciencedirect.com/science/article/pii/S016800720700019XMathSciNetCrossRef

Baaz, M., Zach, R.: Hypersequents and the proof theory of intuitionistic fuzzy logic. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 187–201. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44622-2_12CrossRefMATH

Belnap Jr., N.D.: Display logic. J. Philos. Log. 11(4), 375–417 (1982)MathSciNetCrossRef

Borgwardt, S., Distel, F., Peñaloza, R.: Decidable Gödel description logics without the finitely-valued model property. In: Baral, C., De Giacomo, G., Eiter, T. (eds.) Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR 2014), pp. 228–237. AAAI Press (2014)

Dummett, M.: A propositional calculus with denumerable matrix. J. Symb. Log. 24(2), 97–106 (1959). http://www.jstor.org/stable/2964753MathSciNetCrossRef

Fitting, M.: Nested sequents for intuitionistic logics. Notre Dame J. Form. Log. 55(1), 41–61 (2014). https://doi.org/10.1215/00294527-2377869MathSciNetCrossRefMATH

Gabbay, D., Shehtman, V., Skvortsov, D.: Quantification in Non-classical Logics. Studies in Logic and Foundations of Mathematics. Elsevier, Amsterdam (2009)MATH

10.

Gentzen, G.: Untersuchungen uber das logische schliessen. Math. Z. 39(3), 405–431 (1935)MathSciNetCrossRef

11.

Gödel, K.: Zum intuitionistischen aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien 69, 65–66 (1932)MATH

12.

Goré, R., Postniece, L., Tiu, A.: Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic 7, Papers from the Seventh Conference on “Advances in Modal Logic,” held in Nancy, France, 9–12 September 2008, pp. 43–66. College Publications (2008). http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf

13.

Hajek, P.: The Metamathematics of Fuzzy Logic. Kluwer, Dordrecht (1998)CrossRef

14.

Horn, A.: Logic with truth values in a linearly ordered heyting algebra. J. Symb. Log. 34(3), 395–408 (1969). http://www.jstor.org/stable/2270905MathSciNetCrossRef

15.

Lellmann, B.: Linear nested sequents, 2-sequents and hypersequents. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 135–150. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24312-2_10CrossRefMATH

16.

Lellmann, B.: LNSprover: modular theorem proving with linear nested sequents (2016). https://www.logic.at/staff/lellmann/lnsprover/

17.

Lellmann, B., Kuznets, R.: Interpolation for intermediate logics via hyper- and linear nested sequents. In: Advances in Modal Logic, vol. 12, pp. 473–492 (2018)

18.

Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comput. Log. 2(4), 526–541 (2001). https://doi.org/10.1145/383779.383783MathSciNetCrossRefMATH

19.

Lyon, T.: Syntactic cut-elimination for intuitionistic fuzzy logic via linear nested sequents (2019). https://arxiv.org/abs/1910.06657

20.

Lyon, T., van Berkel, K.: Automating agential reasoning: proof-calculi and syntactic decidability for STIT logics. In: Baldoni, M., Dastani, M., Liao, B., Sakurai, Y., Zalila Wenkstern, R. (eds.) PRIMA 2019. LNCS (LNAI), vol. 11873, pp. 202–218. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-33792-6_13CrossRef

21.

Lyon, T., Tiu, A., Góre, R., Clouston, R.: Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In: Fernández, M., Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 152. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2020, forthcoming)

22.

Masini, A.: 2-sequent calculus: a proof theory of modalities. Ann. Pure Appl. Log. 58(3), 229–246 (1992). https://doi.org/10.1016/0168-0072(92)90029-Y. http://www.sciencedirect.com/science/article/pii/016800729290029YMathSciNetCrossRefMATH

23.

Masini, A.: 2-sequent calculus: intuitionism and natural deduction. J. Log. Comput. 3(5), 533–562 (1993). https://doi.org/10.1093/logcom/3.5.533MathSciNetCrossRefMATH

24.

Poggiolesi, F.: A cut-free simple sequent calculus for modal logic S5. Rev. Symb. Log. 1(1), 3–15 (2008). https://doi.org/10.1017/S1755020308080040MathSciNetCrossRefMATH

25.

Takeuti, G., Titani, S.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. Symb. Log. 49(3), 851–866 (1984). https://doi.org/10.2307/2274139MathSciNetCrossRefMATH

26.

Viganò, L.: Labelled Non-classical Logics. Kluwer Academic Publishers, Dordrecht (2000). With a foreword by Dov M. GabbayCrossRef

27.

Visser, A.: On the completenes principle: a study of provability in heyting’s arithmetic and extensions. Ann. Math. Log. 22(3), 263–295 (1982). https://doi.org/10.1016/0003-4843(82)90024-9. http://www.sciencedirect.com/science/article/pii/0003484382900249CrossRefMATH

28.

Wansing, H.: Sequent calculi for normal modal propositional logics. J. Log. Comput. 4(2), 125–142 (1994). https://doi.org/10.1093/logcom/4.2.125MathSciNetCrossRefMATH

Titel: Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
verfasst von: Tim Lyon
Verlag: Springer International Publishing
Buch: Logical Foundations of Computer Science
Print ISBN: 978-3-030-36754-1

Electronic ISBN: 978-3-030-36755-8

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-36755-8_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner