Hauptsatz for higher order logic
From MaRDI portal
Publication:5549033
Cited in
(23)- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- On Takeuti's early view of the concept of set
- Extended First-Order Logic
- Cut-elimination for quantified conditional logic
- On the convergence of reduction-based and model-based methods in proof theory
- Completeness of type assignment systems with intersection, union, and type quantifiers
- A compact representation of proofs
- A cut-free calculus for second-order Gödel logic
- Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik
- Ein starker Normalisationssatz für die intuitionistische Typentheorie
- Typing and computational properties of lambda expressions
- Abstract deduction and inferential models for type theory
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
- Memories of Kurt Schütte and the logic group in Munich: A personal report
- Extended Curry-Howard terms for second-order logic
- A simple proof that super-consistency implies cut elimination
- Analytic tableaux for higher-order logic with choice
- Mechanized metatheory revisited
- Prawitz, Proofs, and Meaning
- Ein Ausgezeichnetes Modell Für Die Intuitionistische Typenlogik
- Polymorphism and the obstinate circularity of second order logic: a victims' tale
- Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik
- A semantics for \(\lambda \)Prolog
This page was built for publication: Hauptsatz for higher order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5549033)
