On the unity of logic

DOI10.1016/0168-0072(93)90093-SMaRDI QIDQ685059zbMATH OpenOpenAlexFDO

Authors Jean-Yves Girard

Publication date 22 September 1993

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(93)90093-s

zbMATH Keywords

classical logiccut-free Gentzen-type systemintuitionistic logiclinear logicpolarity

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50)

Recommendations

• Cut elimination for the unified logic
• UNIFICATION IN INTERMEDIATE LOGICS
• On the unification of classical, intuitionistic and affine logics
• A focused approach to combining logics
• A new deconstructive logic: linear logic

Cites work

• A new constructive logic: classic logic
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• Linear logic
• Some Syntactical Observations on Linear Logic

Cited in

(58)

• On the algebraic structure of declarative programming languages
• Focusing and polarization in linear, intuitionistic, and classical logics
• Classical logic, storage operators and second-order lambda-calculus
• Semantics of weakening and contraction
• On the linear decoration of intuitionistic derivations
• A general adequacy result for a linear functional language
• A new framework for declarative programming
• A linear logical framework
• Multi-focused proofs with different polarity assignments
• On the logic of unification
• Structural cut elimination. I: Intuitionistic and classical logic
• A sequent calculus for subtyping polymorphic types
• Petri nets, Horn programs, linear logic and vector games
• Multimodal linguistic inference
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• From the universality of mathematical truth to the interoperability of proof systems
• A pure view of ecumenical modalities
• Cut elimination for the unified logic
• On the unity of duality
• Rewritings for polarized multiplicative and exponential proof structures
• Structural focalization
• Kripke semantics for the logic of problems and propositions
• Static typing for a substructural lambda calculus
• Propositional mixed logic: its syntax and semantics
• scientific article; zbMATH DE number 3966049 (Why is no real title available?)
• Information completeness in Nelson algebras of rough sets induced by quasiorders
• The Logic of Bunched Implications
• A new deconstructive logic: linear logic
• A linear/producer/consumer model of classical linear logic
• scientific article; zbMATH DE number 7439427 (Why is no real title available?)
• Dual-context calculi for modal logic
• Multimodal dependent type theory
• A logical analysis of the Anselm's \textit{Unum argumentum} (from \textit{Proslogion})
• On the unification of classical, intuitionistic and affine logics
• Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
• The practice of logical frameworks
• Linear Logic Properly Displayed
• On the semantics of classical disjunction
• Subtractive logic
• Proof theory in the abstract
• An ecumenical notion of entailment
• LNL polycategories and doctrines of linear logic
• Asynchronous functional sessions: cyclic and concurrent
• Hypersequent calculi for intuitionistic logic with classical atoms
• A focused approach to combining logics
• Comparing session type systems derived from linear logic
• Forum: A multiple-conclusion specification logic
• On the logic of UNITY
• Categories for computation in context and unified logic
• Data layout from a type-theoretic perspective
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Gödel's absolute proofs and Girard's ludics: mutual insights
• On combining intuitionistic and S4 modal logic
• Separability and harmony in ecumenical systems
• The quantum monadology
• Lambek calculus with banged atoms for parasitic gaps
• A proof-theoretic approach to the semantics of classical linear logic
• The unity of a Tractarian fact

This page was built for publication: On the unity of logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685059)