2 citations · 4 across the 5 of their papers we have counts for
5 papers
Ultrafilter Extensions for Veltman Semantics
Fèlix Frigola González, Joost J. Joosten, Vicent Navarro Arroyo +1
In this paper, we present a first-order frame condition for interpretability logic and show that the condition is not modally definable. Yet, the frame condition holds both on ILM…
Mechanising Gödel-Löb provability logic in HOL Light
Marco Maggesi, Cosimo Perini Brogi
We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuri…
An analytic calculus for intuitionistic belief
Cosimo Perini Brogi
Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-refl…
A formal proof of modal completeness for provability logic
Marco Maggesi, Cosimo Perini Brogi
This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss som…
Curry-Howard-Lambek Correspondence for Intuitionistic Belief
Cosimo Perini Brogi
This paper introduces a natural deduction calculus for intuitionistic logic of belief which is easily turned into a modal -calculus giving a computational sem…