Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

Fiorino, Guido
Journal of Automated Reasoning , Volume 67 (1) – Mar 1, 2023
Download PDF
28 pages

Loading next page...
 
/lp/springer-journals/linear-depth-deduction-with-subformula-property-for-intuitionistic-Bbzvxc90r0
Publisher
Springer Journals
Copyright
Copyright © The Author(s), under exclusive licence to Springer Nature B.V. 2022. Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1007/s10817-022-09653-z
Publisher site
See Article on Publisher Site

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.

Journal

Journal of Automated Reasoning – Springer Journals

Published: Mar 1, 2023

Keywords: Intuitionistic epistemic logic; Sequent calculi; Subformula property; Counter-models generation

References

  • Intuitionistic epistemic logic
    Artëmov, SN; Protopopescu, T
  • Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
    Ferrari, M; Fiorentini, C; Fiorino, G
  • An evaluation-driven decision procedure for G3i
    Ferrari, M; Fiorentini, C; Fiorino, G
  • Nested sequents for intuitionistic logics
    Fitting, M
  • An O(nlogn)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${O}(n \log n)$$\end{document}- space decision procedure for intuitionistic propositional logic
    Hudelmaier, J