Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
From MaRDI portal
Publication:3244103
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
Cites Work
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)