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 to 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 the invalidity.

Fiorino, G. (2021). Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic [Working paper] [10.48550/arXiv.2103.03377].

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

Fiorino, GG
2021

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 to 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 the invalidity.
Working paper
Scientifica
Mathematics Logic, Mathematics, Logic, 03F03, F.4.1
English
Fiorino, G. (2021). Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic [Working paper] [10.48550/arXiv.2103.03377].
Fiorino, G
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/368938
Citazioni
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
Social impact