Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

DOI10.2307/2963594zbMATH Open0079.24502OpenAlexW2114633883MaRDI QIDQ3244103FDOQ3244103

Authors:

Publication date: 1957

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2963594

zbMATH Keywords

foundations, philosophy, logic

Cites Work

• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Remarks on identity and description in first-order axiom systems

Cited In (only showing first 100 items - show all)

• Semantic interpolation
• The institution-theoretic scope of logic theorems
• The metatheory of the classical propositional calculus is not axiomatizable
• Linear reasoning in modal logic
• Recognizability of all WIP-minimal logics
• Exploiting partial variable assignment in interpolation-based model checking
• The interpolation problem in finite-layered pre-Heyting logics
• Interpolation and amalgamation for arrays with MaxDiff
• Farkas-based tree interpolation
• Algorithms for recognizing restricted interpolation over the modal logic S4
• Common knowledge does not have the Beth property
• On interpolation problem in paraconsistent extensions of the minimal logic
• Lattice-based refinement in bounded model checking
• Machine-checked interpolation theorems for substructural logics using display calculi
• Properties preserved under algebraic constructions
• Weakly equivalent arrays
• A note on constructive interpolation for the multi-modal logic \(K_m\)
• Complete instantiation-based interpolation
• Craig interpolation in the presence of unreliable connectives
• On dynamically generated ontology translators in agent communication
• How QBF expansion makes strategy extraction hard
• SOME MODEL THEORY OF GUARDED NEGATION
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Title not available (Why is that?)
• Modularity results for interpolation, amalgamation and superamalgamation
• The Craig interpolation theorem in abstract model theory
• Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys
• Interpolation in extensions of first-order logic
• Definability for model counting
• Craig interpolation in displayable logics
• Progression of decomposed local-effect action theories
• Multicomponent proof-theoretic method for proving interpolation properties
• Interpolation method for multicomponent sequent calculi
• Decidability of some interpolation properties for weakly transitive modal logics
• Alternative multilattice logics: an approach based on monosequent and indexed monosequent calculi
• Feasible interpolation for QBF resolution calculi
• Learning inductive invariants by sampling from frequency distributions
• Continuum of normal extensions of the modal logic of provability with the interpolation property
• ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS
• On Automorphisms of Polyadic Algebras
• Notes on Craig interpolation for LJ with strong negation
• First-order interpolation derived from propositional interpolation
• Classification of extensions of the modal logic S4
• Embedding friendly first-order paradefinite and connexive logics
• Consistency-preserving refactoring of refinement structures in Event-B models
• A note on the interpolation property in tense logic
• Temporal logics of “the next” do not have the beth property
• Semantical criteria of empirical meaningfulness
• A configurable CEGAR framework with interpolation-based refinements
• Definibility in normal theories
• \(\mathrm{NL}_\lambda\) as the logic of scope and movement
• Interpolation-based GR(1) assumptions refinement
• Joint consistency in extensions of the minimal logic
• Hybrid extensions of the minimal logic
• Interpolation and definability over the logic Gl
• Decidability of the weak interpolation property over the minimal logic
• Interpolation and the projective Beth property in well-composed logics
• Algorithmic introduction of quantified cuts
• Failure of interpolation in combined modal logics
• Causality-based game solving
• Interpolation and model checking for nonlinear arithmetic
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Resolution proof transformation for compression and interpolation
• Nondeterministic functions and the existence of optimal proof systems
• Beth definability, interpolation and language splitting
• On propositional definability
• Whale: an interpolation-based algorithm for inter-procedural verification
• Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
• Intuitionistic logic and implicit definability
• The road to two theorems of logic
• Interpolation and Symbol Elimination
• Proof tree preserving tree interpolation
• Proof complexity of non-classical logics
• Horn clause solvers for program verification
• The decidability of Craig's interpolation property in well-composed J-logics
• Quantifier-free interpolation in combinations of equality interpolating theories
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• An extension of lazy abstraction with interpolation for programs with arrays
• Perceptibility in pre-Heyting logics
• Title not available (Why is that?)
• Interpolation in weakly transitive modal logics
• On Languages Which are Based on Non-Standard Arithmetic
• Toward a theory of the process of explanation
• Benchmarking a model checker for algorithmic improvements and tuning for performance
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Harmonious logic: Craig's interpolation theorem and its descendants
• Partition-based logical reasoning for first-order and propositional theories
• Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras
• On a generalized modularization theorem
• Minding the is-ought gap
• Amalgamation, interpolation, and implicit definability in varieties of algebras
• The Lyndon property and uniform interpolation over the Grzegorczyk logic
• Interpolation theorems in modal logics. Sufficient conditions
• Der Interpolationssatz der intuitionistischen Prädikatenlogik
• Satisfiability modulo theories
• Refining abstract interpretations
• Satisfaction for n-th order languages defined in n-th order languages
• Definability theorems in normal extensions of the provability logic

This page was built for publication: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

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