Related papers: A Real-Valued Modal Logic
Recent years witness a growing interest in nonstandard epistemic logics of "knowing whether", "knowing what", "knowing how", and so on. These logics are usually not normal, i.e., the standard axioms and reasoning rules for modal logic may…
This paper introduces higher-order (``nested") Kripke models, a generalization of Kripke models that is remarkably close to Kripke's original idea -- both mathematically and conceptually. Standard models are now $0$-ary models, whereas…
\textbf{T-BAT} logic is a formal system designed to express the notion of informal provability. This type of provability is closely related to mathematical practice and is quite often contrasted with formal provability, understood as a…
This paper studies nested sequents for quantified modal logics. In particular, it considers extensions of the propositional modal logics definable by the axioms D, T, B, 4, and 5 with varying, increasing, decreasing, and constant domains.…
The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible…
We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for…
Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality $!_r$ captures how many times a…
We give a calculus for reasoning about the first-order fragment of classical logic that is adequate for giving the truth conditions of intuitionistic Kripke frames, and outline a proof-theoretic soundness and completeness proof, which we…
The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems,…
Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator [18] was introduced to formalise programs running in parallel. In other direction, other authors proposed a systematic…
We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the…
We define the notion of a model of higher-order modal logic in an arbitrary elementary topos $\mathcal{E}$. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the…
We introduce two modal natural deduction systems that are suitable to represent and reason about transformations of quantum registers in an abstract, qualitative, way. Quantum registers represent quantum systems, and can be viewed as the…
Within the possibilistic approach to uncertainty modeling, the paper presents a modal logical system to reason about qualitative (comparative) statements of the possibility (and necessity) of fuzzy propositions. We relate this qualitative…
We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the…
It is known that many modal and superintuitionistic logics are PSPACE-hard in languages with a small number of variables; however, questions about the complexity of similar fragments of many logics obtained by adding various axioms to…
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for…
The Kripke semantics of various logics arises via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational…
A non-distributive two-sorted hypersequent calculus \textbf{PDBL} and its modal extension \textbf{MPDBL} are proposed for the classes of pure double Boolean algebras and pure double Boolean algebras with operators respectively. A relational…
In this paper, we investigate arithmetical completeness with respect to finite Kripke models of quantified modal logic. We adapt the finite-model embedding techniques of Artemov and Japaridze to two settings involving finite Kripke models.…