Display logic

Publication date: 1982

Published in: Journal of Philosophical Logic (Search for Journal in Brave)

proof theory connective intuitionistic logic modal logics combinatory logic necessity impossibility Gentzen-style calculus elimination theorem intensional conjunction boolean connectives monadic operator nested implication

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items

Current trends in substructural logics, Paraconsistent logic, Power and Limits of Structural Display Rules, Linear Logic Properly Displayed, Deep sequent systems for modal logic, Logicality, double-line rules, and modalities, A formally verified cut-elimination procedure for linear nested sequents for tense logic, Syntactic Completeness of Proper Display Calculi, A Unified Display Proof Theory for Bunched Logic, Hypersequent rules with restricted contexts for propositional modal logics, Indexed systems of sequents and cut-elimination, THE LOGIC OF RESOURCES AND CAPABILITIES, Multimodal linguistic inference, Non-normal modal logics and conditional logics: semantic analysis and proof theory, A comparison between monoidal and substructural logics, LINEAR TIME IN HYPERSEQUENT FRAMEWORK, Some general results about proof normalization, Rooted hypersequent calculus for modal logic \textsf{S5}, Bunched logics displayed, Disentangling structural connectives or life without display property, The nature of entailment: an informational approach, THE LOGIC OF HYPERLOGIC. PART A: FOUNDATIONS, Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus, Proof search and co-NP completeness for many-valued logics, Strong and Weak Quantifiers in Focused NL$$_{\text {CL}}$$, Explorations in Subexponential Non-associative Non-commutative Linear Logic, An algebraic glimpse at bunched implications and separation logic, Restall's proof-theoretic pluralism and relevance logic, Monoidal logics: completeness and classical systems, Lattice logic as a fragment of (2-sorted) residuated modal logic, Knowledge, belief, normality, and introspection, Hypersequent Calculi for S5: The Methods of Cut Elimination, Sufficient conditions for cut elimination with complexity analysis, Machine-Checked Proof-Theory for Propositional Modal Logics, A perspective on modal sequent logic, Craig Interpolation in Displayable Logics, BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS, Understanding negation implicationally in the relevant logic R, Solution to a problem of Ono and Komori, Normal proofs, cut free derivations and structural rules, Hypersequent and display calculi -- a unified perspective, A survey of nonstandard sequent calculi, Combining linear-time temporal logic with constructiveness and paraconsistency, Cut-elimination for weak Grzegorczyk logic Go, A generalized proof-theoretic approach to logical argumentation based on hypersequents, Unnamed Item, Display calculi and other modal calculi: a comparison, On Displaying Negative Modalities, Unnamed Item, Judgmental subtyping systems with intersection types and modal types, Algebraic proof theory: hypersequents and hypercompletions, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information, Types as graphs: Continuations in type logical grammar, Unnamed Item, Prawitz, Proofs, and Meaning, A cut-elimination proof in positive relevant logic with necessity, Focused and Synthetic Nested Sequents, Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi, Displaying and deciding substructural logics. I: Logics with contraposition, On a multilattice analogue of a hypersequent S5 calculus, A Multi-type Calculus for Inquisitive Logic, Solution to a problem of Ono and Komori, Proof theory of Nelson's paraconsistent logic: a uniform perspective, A proof-theoretic approach to negative translations in intuitionistic tense logics, Bilattice logic properly displayed, Unnamed Item, Non-associative, non-commutative multi-modal linear logic, R-Mingle is Nice, and so is Arnon Avron, Simple consequence relations, On purported Gentzen formulations of two positive relevant logics, Cut elimination inside a deep inference system for classical predicate logic, Towards a semantic characterization of cut-elimination