Skip to Main content Skip to Navigation
New interface
Documents associated with scientific events

Justification logic for constructive modal logic *

Roman Kuznets 1 Sonia Marin 2 Lutz Strassburger 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 metadata

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01614707
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Wednesday, October 11, 2017 - 12:04:30 PM
Last modification on : Wednesday, February 2, 2022 - 3:57:52 PM
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 Strassburger. 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

394

Files downloads

226