A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms

DOI10.1007/978-3-540-87531-4_14zbMath1157.03031OpenAlexW1573969001MaRDI QIDQ3540178

Olivier Hermant, James Lipton

Publication date: 20 November 2008

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-87531-4_14

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (1)

A simple proof that super-consistency implies cut elimination

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume II
• Theorem proving modulo
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• 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
• Uniform proofs as a foundation for logic programming
• A remark on free choice sequences and the topological completeness proofs
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Syntactical and semantical properties of simple type theory
• Another intuitionistic completeness proof
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• Proof normalization modulo
• Hauptsatz for higher order logic
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Resolution in type theory
• On weak completeness of intuitionistic predicate logic
• A formulation of the simple theory of types

This page was built for publication: A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms