nach oben

Tipp

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

verfasst von: Guido Fiorino

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2023

Einloggen, um Zugang zu erhalten

Abstract

In their seminal paper Artemov and Protopopescu provide Hilbert formal systems, Brower–Heyting–Kolmogorov and Kripke semantics for the logics of intuitionistic belief and knowledge. Subsequently Krupski has proved that the logic of intuitionistic knowledge is PSPACE-complete and Su and Sano have provided calculi enjoying the subformula property. This paper continues the investigations around sequent calculi for Intuitionistic Epistemic Logics by providing sequent calculi that have the subformula property and that are terminating in linear depth. Our calculi allow us to design a procedure that for invalid formulas returns a Kripke model of minimal depth. Finally we also discuss refutational sequent calculi, that is sequent calculi to prove that formulas are invalid.

Vorheriger Artikel Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

Nächster Artikel A Solver for Arrays with Concatenation

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Artëmov, S.N., Protopopescu, T.: Intuitionistic epistemic logic. Rev. Symb. Log. 9(2), 266–298 (2016). https://doi.org/10.1017/S1755020315000374 MathSciNetCrossRefMATH

Brogi, C.P.: Curry-howard-lambek correspondence for intuitionistic belief. CoRR (2020). arXiv:2006.02417

Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997) MATH

Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Automated Reason. 51(2), 129–149 (2013). https://doi.org/10.1007/s10817-012-9252-7 MathSciNetCrossRefMATH

Ferrari, M., Fiorentini, C., Fiorino, G.: An evaluation-driven decision procedure for G3i. ACM Trans. Comput. Logic 6(1), 8:1-8:37 (2015) MathSciNetMATH

Fitting, M.: Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam (1969) MATH

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

Hudelmaier, J.: An \({O}(n \log n)\)- space decision procedure for intuitionistic propositional logic. J. Logic Comput. 3(1), 63–75 (1993) MathSciNetCrossRefMATH

Krupski, V.N., Yatmanov, A.: Sequent calculus for intuitionistic epistemic logic IEL. In: Artëmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science—International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4–7, 2016. Proceedings, Lecture Notes in Computer Science, vol. 9537, pp. 187–201. Springer (2016). https://doi.org/10.1007/978-3-319-27683-0_14

10.

Rogozin, D.: Modal type theory based on the intuitionistic modal logic \(\textbf{IEL}\). In: Artëmov, S.N., Nerode, A. (eds.) Logical Foundations of Computer Science—International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4–7, 2020, Proceedings, Lecture Notes in Computer Science, vol. 11972, pp. 236–248. Springer (2020). https://doi.org/10.1007/978-3-030-36755-8_15

11.

Su, Y., Sano, K.: First-order intuitionistic epistemic logic. In: Blackburn, P., Lorini, E., Guo, M. (eds.) Logic, Rationality, and Interaction—7th International Workshop, LORI 2019, Chongqing, China, October 18-21, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11813, pp. 326–339. Springer (2019). https://doi.org/10.1007/978-3-662-60292-8_24

12.

Troelstra, A., van Dalen, D.: Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics, vol. 121. North-Holland, Amsterdam (1988) MATH

13.

Troelstra, A., Schwichtenberg, H.: Basic Proof Theory, vol. 43. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1996) MATH

14.

Vorob’ev, N.N.: A new algorithm of derivability in a constructive calculus of statements. In: Sixteen papers on logic and algebra. American Mathematical Society Translations, Series 2, vol. 94, pp. 37–71. American Mathematical Society, Providence (1970)

Titel: Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
verfasst von: Guido Fiorino
Publikationsdatum: 01.03.2023
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2023
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-022-09653-z

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2023

Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

Measuring the Readability of Geometric Proofs: The Area Method Case

Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

Efficient Extensional Binary Tries

Superposition for Higher-Order Logic

A Formalization and Proof Checker for Isabelle’s Metalogic

Premium Partner