Justification logic for constructive modal logic *

Roman Kuznets 1 Sonia Marin 2 Lutz Straßburger 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We provide a treatement of the intuitionistic 3 modality in the style of justification logic. We introduce a new type of terms, called witness terms, that justify consistency, obtain justification analogs for the constructive modal logics CK, CD, CT, and CS4, and prove the realization theorem for them.
Document type :
Documents associated with scientific events
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01614707
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, October 11, 2017 - 12:04:30 PM
Last modification on : Sunday, December 22, 2019 - 2:38:37 AM
Long-term archiving on: Friday, January 12, 2018 - 1:48:20 PM

File

main-IMLAversion.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01614707, version 1

Citation

Roman Kuznets, Sonia Marin, Lutz Straßburger. Justification logic for constructive modal logic *. IMLA 2017 - 7th Workshop on Intuitionistic Modal Logic and Applications, Jul 2017, Toulouse, France. 2017. ⟨hal-01614707⟩

Share

Metrics

Record views

367

Files downloads

114