scientific article; zbMATH DE number 786494

zbMath0829.03031MaRDI QIDQ4842975

Harold Schellinx, Vincent Danos, Jean-Baptiste Joinet

Publication date: 16 August 1995

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

linear logicintuitionistic logicsecond-order propositional logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (22)

From axioms to synthetic inference rules via focusing ⋮ Polarized games ⋮ Proof checking and logic programming ⋮ On the linear decoration of intuitionistic derivations ⋮ Categorical proof theory of classical propositional calculus ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A semantic framework for proof evidence ⋮ Game-theoretic analysis of call-by-value computation ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Unnamed Item ⋮ Classical Call-by-Need and Duality ⋮ Multi-focused proofs with different polarity assignments ⋮ Strong normalization for all-style LKtq ⋮ Yet another bijection between sequent calculus and natural deduction ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ Proof Checking and Logic Programming ⋮ A framework for proof systems ⋮ Proof theory in the abstract ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus ⋮ Focusing and polarization in linear, intuitionistic, and classical logics ⋮ Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory

This page was built for publication: