On the Convergence of Reduction-based and Model-based Methods in Proof Theory

DOI10.1016/j.entcs.2008.03.070zbMath1277.03056OpenAlexW2081888967MaRDI QIDQ2866742

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

modelscut eliminationreducibility candidatestruth-values algebras

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Theorem proving modulo
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• A proof of cut-elimination theorem in simple type-theory
• About Folding-Unfolding Cuts and Cuts Modulo
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Superdeduction at Work
• Truth Values Algebras and Proof Normalization
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Stratification and cut-elimination
• Proof normalization modulo
• A Simple Proof That Super-Consistency Implies Cut Elimination
• Hauptsatz for higher order logic
• Intensional interpretations of functionals of finite type I
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Resolution in type theory
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications

This page was built for publication: On the Convergence of Reduction-based and Model-based Methods in Proof Theory