nach oben

Journal of Automated Reasoning

Erschienen in:

01.03.2023

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

verfasst von: Guido Fiorino

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

Einloggen

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

search-config

KI-gestützte Suche

Aus

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 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 "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

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

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

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-7MathSciNetCrossRefMATH

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-2377869MathSciNetCrossRefMATH

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

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 "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2023

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Efficient Extensional Binary Tries

Superposition for Higher-Order Logic

Finding Normal Binary Floating-Point Factors Efficiently

A Solver for Arrays with Concatenation

Computer-Aided Constructions of Commafree Codes