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
• Through an inference rule, darkly
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Abstract Counterexamples for Non-disjunctive Abstractions
• Some applications of propositional logic to cellular automata
• Maksimova, relevance and the study of lattices of non-classical logics
• Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
• (Heterogeneous) structured specifications in logics without interpolation
• A proof theoretic proof of Scott's general interpolation theorem
• Eine Semantische Charakterisierung der Durch die Implikation Allein Darstellbaren Wahrheitsfunktionen
• Craig Interpolation for Linear Temporal Languages
• Generalized interpolation theorems
• SMT-based verification of program changes through summary repair
• On enumerating query plans using analytic tableau
• Effective interpolation and preservation in guarded logics
• On interpolation when function symbols are present
• The logic of secrets and the interpolation rule
• Rewriting interpolants
• From choosing elements to choosing concepts: the evolution of Feferman's work in model theory
• Interpolation Results for Arrays with Length and MaxDiff
• Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
• Craig interpolation for decidable first-order fragments
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• Craig interpolation with clausal first-order tableaux
• Craig's interpolation property in pretabular logics
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Combining Model Checking and Deduction
• Common equivalence and size of forgetting from Horn formulae
• Partial quantifier elimination and property generation
• The \textsc{Golem} Horn solver
• Transition power abstractions for deep counterexample detection
• Pretabularity and Craig's interpolation property
• Range-restricted and Horn interpolation through clausal tableaux
• Pretabularity and Craig's interpolation problem over the minimal logic
• Differentiable learning of matricized DNFs and its application to Boolean networks
• 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

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)