Propositional lax logic

DOI10.1006/inco.1997.2627zbMath0889.03015OpenAlexW2023132547MaRDI QIDQ1368378

Matt Fairtlough, Michael Mendler

Publication date: 26 November 1997

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/65c39e5ab7529695b9d68b88ae759c7a27b2503e

zbMATH Keywords

Kripke modelspropositional modal logichardware verificationintuitionistic modal logicperformance evaluation of computer hardware

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Abstract deductive systems (03B22) Other applications of logic (03B80)

Related Items

Jankov Formulas and Axiomatization Techniques for Intermediate Logics ⋮ A dual-context sequent calculus for the constructive modal logic S4 ⋮ Intuitionistic non-normal modal logics: a general framework ⋮ Game semantics for constructive modal logic ⋮ The Došen square under construction: a tale of four modalities ⋮ Back to futures ⋮ Logic in Access Control (Tutorial Notes) ⋮ Embedding Constructive K into Intuitionistic K ⋮ Diego's theorem for nuclear implicative semilattices ⋮ An intuitionistic reformulation of Mally's deontic logic ⋮ Three roads to complete lattices: orders, compatibility, polarity ⋮ Correspondence theory for modal Fairtlough-Mendler semantics of intuitionistic modal logic ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Deriving dualities in pointfree topology from Priestley duality ⋮ Admissible rules for six intuitionistic modal logics ⋮ Cardinality reduction theorem for logics QHC and QH4 ⋮ Topological models of propositional logic of problems and propositions ⋮ Morpho-logic from a topos perspective -- application to symbolic AI ⋮ B-frame duality ⋮ The Cooper storage idiom ⋮ Constructive Boolean circuits and the exactness of timed ternary simulation ⋮ Mathematical modal logic: A view of its evolution ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ A framework for linear authorization logics ⋮ A semantic hierarchy for intuitionistic logic ⋮ Fibrational modal type theory ⋮ Proofs and countermodels in non-classical logics ⋮ 2003 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquim '03 ⋮ Logic of subtyping ⋮ A general method for proving decidability of intuitionistic modal logics ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Unnamed Item ⋮ Proof search and certificates for evidential transactions ⋮ A Kuroda-style \(j\)-translation ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ Constructive linear-time temporal logic: proof systems and Kripke semantics ⋮ Algebraic semantics of the \(\left\{ \rightarrow ,\square \right\} \)-fragment of propositional lax logic ⋮ Constructive Modalities with Provability Smack ⋮ Access Control in a Core Calculus of Dependency ⋮ On modal logics of partial recursive functions

Uses Software

• Haskell

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Some results on intermediate constructive logics
• Notions of computation and monads
• Proof methods for modal and intuitionistic logics
• On maximal intermediate logics with the disjunction property
• Topoi. The categorial analysis of logic
• Modal operators on Heyting algebras
• Constructivism in mathematics. An introduction. Volume I
• Eine Unableitbarkeitsbeweismethode für den Intuitionistischen Aussagenkalkül
• Intuitionistic tense and modal logic
• Grothendieck Topology as Geometric Modality
• Almost duplication-free tableau calculi for prepositional lax logics
• A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property
• The elimination theorem when modality is present