Intuitionistic Modal Logic: A 15-year retrospective

2015 ◽  
Vol 28 (5) ◽  
pp. 873-882 ◽  
Author(s):  
Charles Stewart ◽  
Valeria de Paiva ◽  
Natasha Alechina
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

scholarly journals Intuitionistic Modal Logic and Applications (IMLA 2008)

2011 ◽  
Vol 209 (12) ◽  
pp. 1435-1436
Author(s):  
Valeria de Paiva ◽  
Brigitte Pientka
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

scholarly journals A bi-intuitionistic modal logic: Foundations and automation

2016 ◽  
Vol 85 (4) ◽  
pp. 500-519 ◽  
Author(s):  
John G. Stell ◽  
Renate A. Schmidt ◽  
David Rydeheard
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

□ In intuitionistic modal logic

1997 ◽  
Vol 75 (2) ◽  
pp. 201-213 ◽  
Author(s):  
David DeVidi ◽  
Graham Solomon
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

Characterising combinational timing analyses in intuitionistic modal logic

2000 ◽  
Vol 8 (6) ◽  
pp. 821-852 ◽  
Author(s):  
M Mendler
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

Categorical and algebraic aspects of the intuitionistic modal logic IEL― and its predicate extensions

2020 ◽  
Author(s):  
Daniel Rogozin
Keyword(s):  
Modal Logic ◽  
Type Theory ◽  
Lambda Calculus ◽  
Conference Paper ◽  
Logical Foundations ◽  
Intuitionistic Modal Logic ◽  
Monoidal Functor ◽  
Cover Systems ◽  
Cartesian Closed ◽  
Intuitionistic Version

Abstract The system of intuitionistic modal logic $\textbf{IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic (S. Artemov and T. Protopopescu. Intuitionistic epistemic logic. The Review of Symbolic Logic, 9, 266–298, 2016). We construct the modal lambda calculus, which is Curry–Howard isomorphic to $\textbf{IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming.We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a Cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operators. Such operators are used in point-free topology as well. We study complete Kripke–Joyal-style semantics for predicate extensions of $\textbf{IEL}^{-}$ and related logics using Dedekind–MacNeille completions and modal cover systems introduced by Goldblatt (R. Goldblatt. Cover semantics for quantified lax logic. Journal of Logic and Computation, 21, 1035–1063, 2011). The paper extends the conference paper published in the LFCS’20 volume (D. Rogozin. Modal type theory based on the intuitionistic modal logic IEL. In International Symposium on Logical Foundations of Computer Science, pp. 236–248. Springer, 2020).

Intuitionistic Modal Logic

1999 ◽  
pp. 227-238 ◽  
Author(s):  
Frank Wolter ◽  
Michael Zakharyaschev
Keyword(s):  
Modal Logic ◽  
Intuitionistic Modal Logic

scholarly journals A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Ki Yung Ahn ◽  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Modal Logic ◽  
Modal Logics ◽  
Completeness Proof ◽  
Intuitionistic Modal Logic ◽  
Free Variables ◽  
Open Process ◽  
Intuitionistic Modal Logics

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.

Sign in / Sign up

Export Citation Format

Share Document