A new constructive logic: classic logic
From MaRDI portal
Publication:4006233
DOI10.1017/S0960129500001328zbMath0752.03027OpenAlexW1985185257MaRDI QIDQ4006233
Publication date: 26 September 1992
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129500001328
coherent spacescorrelation spaceGentzen-type system LC for classical first order predicate logicnegative translation of classical logic into intuitionistic logicsemantics for derivations in \(LC\)semantics for derivations in LC
Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (70)
Classical logic, storage operators and second-order lambda-calculus ⋮ Models of Linear Logic based on the Schwartz $\varepsilon$-product ⋮ Cut elimination for the unified logic ⋮ Semantics of weakening and contraction ⋮ True concurrency semantics for a linear logic programming language with broadcast communication ⋮ Polarized games ⋮ Proof checking and logic programming ⋮ A Categorical Setting for Lower Complexity ⋮ A pure view of ecumenical modalities ⋮ Petri nets, Horn programs, linear logic and vector games ⋮ Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less) ⋮ A micrological study of negation ⋮ A categorical semantics for polarized MALL ⋮ Games and full completeness for multiplicative linear logic ⋮ Jump from parallel to sequential proofs: exponentials ⋮ Safe recursion revisited. I: Categorical semantics for lower complexity ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Computational isomorphisms in classical logic ⋮ Linear logic and elementary time ⋮ A semantic framework for proof evidence ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ Resource modalities in tensor logic ⋮ Classical proof forestry ⋮ A focused approach to combining logics ⋮ Two loop detection mechanisms: A comparison ⋮ Unnamed Item ⋮ An Indexed System for Multiplicative Additive Polarized Linear Logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proof nets for classical logic ⋮ A proof-theoretic foundation of abortive continuations ⋮ A new deconstructive logic: linear logic ⋮ Classical realizability in the CPS target language ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ On the unity of logic ⋮ Proofs of strong normalisation for second order classical natural deduction ⋮ Towards Hilbert's 24th Problem: Combinatorial Proof Invariants ⋮ Preface to the special volume ⋮ On the unity of duality ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Total sets and objects in domain theory ⋮ Proof Checking and Logic Programming ⋮ Subtractive logic ⋮ Polarized and focalized linear and classical proofs ⋮ Unnamed Item ⋮ A phase semantics for polarized linear logic and second order conservativity ⋮ Non-commutative proof construction: a constraint-based approach ⋮ Proof theory in the abstract ⋮ The multiplicative-additive Lambek calculus with subexponential and bracket modalities ⋮ Call-By-Push-Value from a Linear Logic Point of View ⋮ On geometry of interaction for polarized linear logic ⋮ Differential Linear Logic and Polarization ⋮ About classical logic and imperative programming ⋮ Constructive negation, implication, and co-implication ⋮ Enriching an Effect Calculus with Linear Types ⋮ Focalisation and Classical Realisability ⋮ On the unification of classical, intuitionistic and affine logics ⋮ Focusing and polarization in linear, intuitionistic, and classical logics ⋮ Unnamed Item ⋮ A proof theory for model checking ⋮ Proof diagrams for multiplicative linear logic: syntax and semantics ⋮ CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS ⋮ Syntax vs. semantics: A polarized approach ⋮ Proofs, Reasoning and the Metamorphosis of Logic ⋮ Polarized proof-nets and \(\lambda \mu\)-calculus ⋮ The Sequent Calculus of Skew Monoidal Categories ⋮ Quantitative classical realizability ⋮ The additive multiboxes ⋮ Infinitary affine proofs ⋮ Propositions as sessions
Cites Work
This page was built for publication: A new constructive logic: classic logic
