On the convergence of reduction-based and model-based methods in proof theory

DOI10.1016/J.ENTCS.2008.03.070MaRDI QIDQ2866742zbMATH OpenOpenAlexFDO

Authors Gilles Dowek

Publication date 13 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.03.070

zbMATH Keywords

cut eliminationmodelsreducibility candidatestruth-values algebras

Mathematics Subject Classification ID

Applications of model theory (03C98) Cut-elimination and normal-form theorems (03F05)

Recommendations

• On the convergence of reduction-based and model-based methods in proof theory
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Methods of cut-elimination
• Reducing redundancy in cut-elimination by resolution
• Cut-elimination: syntax and semantics

Cites work

• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• A proof of cut-elimination theorem in simple type-theory
• A Simple Proof That Super-Consistency Implies Cut Elimination
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• About folding-unfolding cuts and cuts modulo
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Hauptsatz for higher order logic
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Proof normalization modulo
• Resolution in type theory
• Stratification and cut-elimination
• Superdeduction at Work
• Term Rewriting and Applications
• Theorem proving modulo
• Truth Values Algebras and Proof Normalization
• Typed Lambda Calculi and Applications

Cited in

(1)

• On the convergence of reduction-based and model-based methods in proof theory

This page was built for publication: On the convergence of reduction-based and model-based methods in proof theory

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