scientific article; zbMATH DE number 786494
From MaRDI portal
Publication:4842975
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.
Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
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
