Untersuchungen �ber das logische Schlie�en. I

1935/12/01 by Gerhard Gentzen · 2,031 citations
Arts and Humanities · Mathematics · #German Literature and Culture Studies #History and Theory of Mathematics #Mathematics

paper · doi:10.1007/bf01201353

published in Mathematische Zeitschrift 39(1), 176-210 (Springer Science+Business Media)

openalex publication_date 1935/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05

Cited by

• 'Yes and no'
• Grokking the Sequent Calculus (Functional Pearl)
• Logic-Guided Socially-aware Robot Navigation World Model
• Ordered Adjoint Logic
• Subreflexive Logic: Completeness without Identity
• Resource control and intersection types: an intrinsic connection
• Machine Learning Guidance and Proof Certification for Connection Tableaux
• The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
• Combinatorial Proofs and Decomposition Theorems for First-order Logic
• Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
• Interpolation in Non-Classical Logics
• Probing the "Psyche'' of Large Reasoning Models: Understanding Through a Human Lens
• Intuitionistic Mathematics and Logic
• The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
• Semantic Properties of Computations Defined by Elementary Inference Systems
• Tableau vs. Sequent Calculi for Minimal Entailment
• Yet Another Proof of Glivenko's Theorem
• On Permuting Cut with Contraction
• Common knowledge logic in a higher order proof assistant?
• An essay on msic-systems
• Sequent-Type Proof Systems for Three-Valued Default Logic
• Planning Argumentative Texts
• Characterizing Propositional Proofs as Non-Commutative Formulas
• The Power of Regular Constraint Propagation (Technical Report)
• Strategy Preserving Compilation for Parallel Functional Code
• Functionals and hardware
• On the computational complexity of cut-reduction
• Judgment aggregation in non-classical logics
• Admissibility via Natural Dualities
• From Quantum Metalanguage to the Logic of Qubits
• SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
• LISA -- A Modern Proof System
• Interpolation and Quantifiers in Ortholattices
• Proof-Theoretic Functional Completeness for the Connexive Logic C
• Intuitionistic Euler-Venn Diagrams (extended)
• A sequent calculus demonstration of Herbrand's theorem
• Introducing Quantified Cuts in Logic with Equality
• Peano Arithmetic and μMALL
• Sequent-systems and groupoid models. II
• Sequent-systems and groupoid models. I
• Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
• On the complexity of stratified logics
• On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
• Infinitary Action Logic with Exponentiation
• Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version)
• Resource control and strong normalisation
• Proof Compression via Subatomic Logic and Guarded Substitutions
• Disjunction and existence properties in modal arithmetic
• The Disjunction Property for Operational Relevance Logics
• Computational Complexity of Deciding Provability in Linear Logic and its Fragments
• A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
• Rough sets semantics for the three-valued extension of first-order Priest's da Costa logic
• ProofBuddy: How it Started, How it's Going
• Propositions in Linear Multirole Logic as Multiparty Session Types
• The aim and validity of inference and argument
• Everything old is new again: Quoted Domain Specific Languages
• Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP
• Stoic Sequent Logic and Proof Theory
• On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics
• On Closed Elements in Closure Algebras
• On the Graphical Representation of Proofs as Trees
• P is not equal to NP
• Coherent Bicartesian and Sesquicartesian Categories
• A Proof Method for Quantification Theory: Its Justification and Realization
• DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
• Stellar Resolution: Multiplicatives
• A journey through resource control lambda calculi and explicit substitution using intersection types (an account)
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• Propositions as types
• Advanced Many-Valued Logics
• Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic
• Proof theory for minimal quantum logic I
• Resolution on formula-trees
• Proving Correctness of Graph Programs Relative to Recursively Nested Conditions
• Hilbert's Program Then and Now
• A Constructive Logic with Classical Proofs and Refutations (Extended Version)
• Sequent [wikipedia]
• Sequent calculus [wikipedia]
• Suppes–Lemmon notation [wikipedia]
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description) [europepmc]
• Integrating Induction and Coinduction via Closure Operators and Proof Cycles [europepmc]