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

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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 : Thursday, March 5, 2020 - 6:29:58 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

Collections

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

397

Files downloads

141