Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
From MaRDI portal
Publication:3244103
DOI10.2307/2963594zbMath0079.24502OpenAlexW2114633883MaRDI QIDQ3244103
No author found.
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
Related Items (only showing first 100 items - show all)
Hybrid extensions of the minimal logic ⋮ Algorithms for recognizing restricted interpolation over the modal logic S4 ⋮ Extensions of the minimal logic and the interpolation problem ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Proof tree preserving tree interpolation ⋮ Causality-based game solving ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ A note on constructive interpolation for the multi-modal logic \(K_m\) ⋮ Lattice-based refinement in bounded model checking ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Notes on Craig interpolation for LJ with strong negation ⋮ Semantic interpolation ⋮ Satisfiability Modulo Theories ⋮ Combining Model Checking and Deduction ⋮ On Enumerating Query Plans Using Analytic Tableau ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ Recognizability of all WIP-minimal logics ⋮ On propositional definability ⋮ A note on the interpolation property in tense logic ⋮ Joint consistency in extensions of the minimal logic ⋮ Craig interpolation with clausal first-order tableaux ⋮ The projective Beth property in well-composed logics ⋮ Observing, reporting, and deciding in networks of sentences ⋮ Der Interpolationssatz der intuitionistischen Prädikatenlogik ⋮ Horn Clause Solvers for Program Verification ⋮ Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Interpolation in extensions of first-order logic ⋮ Consistency-preserving refactoring of refinement structures in Event-B models ⋮ Algorithmic introduction of quantified cuts ⋮ Interpolation properties of superintuitionistic logics ⋮ The decidability of Craig's interpolation property in well-composed J-logics ⋮ First-order interpolation derived from propositional interpolation ⋮ \(\mathrm{NL}_\lambda\) as the logic of scope and movement ⋮ Interpolation theorems in modal logics and amalgamable varieties of topological Boolean algebras ⋮ Weakly Equivalent Arrays ⋮ Perceptibility in pre-Heyting logics ⋮ Decidability of the interpolation problem and of related properties in tabular logics ⋮ Projective Beth property in extensions of Grzegorczyk logic ⋮ Craig interpolation for networks of sentences ⋮ Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces ⋮ Properties preserved under algebraic constructions ⋮ Interpolation theorems in modal logics. Sufficient conditions ⋮ Classification of extensions of the modal logic S4 ⋮ 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 ⋮ Interpolation and definability over the logic Gl ⋮ Definability theorems in normal extensions of the provability logic ⋮ Continuum of normal extensions of the modal logic of provability with the interpolation property ⋮ An Interpolation Theorem ⋮ The Lyndon property and uniform interpolation over the Grzegorczyk logic ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Resolution proof transformation for compression and interpolation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Farkas-based tree interpolation ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ Through an Inference Rule, Darkly ⋮ Interpolation over the minimal logic and Odintsov intervals ⋮ On dynamically generated ontology translators in agent communication ⋮ Craig Interpolation in Displayable Logics ⋮ SMT-based model checking for recursive programs ⋮ Hybrid logics: characterization, interpolation and complexity ⋮ The institution-theoretic scope of logic theorems ⋮ Craig interpolation in the presence of unreliable connectives ⋮ Interpolation in weakly transitive modal logics ⋮ Interpolation and the projective Beth property in well-composed logics ⋮ Decidability of the weak interpolation property over the minimal logic ⋮ Beth definability, interpolation and language splitting ⋮ Exploiting partial variable assignment in interpolation-based model checking ⋮ The interpolation problem in finite-layered pre-Heyting logics ⋮ Semantical criteria of empirical meaningfulness ⋮ Definability and interpolation in non-classical logics ⋮ Common knowledge does not have the Beth property ⋮ Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ Minding the is-ought gap ⋮ Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras ⋮ Amalgamation, interpolation, and implicit definability in varieties of algebras ⋮ Definability for model counting ⋮ Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi ⋮ Relational Decomposition ⋮ The road to two theorems of logic ⋮ Harmonious logic: Craig's interpolation theorem and its descendants ⋮ The Craig interpolation theorem in abstract model theory ⋮ Alternative multilattice logics: an approach based on monosequent and indexed monosequent calculi ⋮ A Configurable CEGAR Framework with Interpolation-Based Refinements ⋮ Refining abstract interpretations ⋮ Amalgamation, congruence-extension, and interpolation properties in algebras ⋮ Definibility in normal theories ⋮ Embedding friendly first-order paradefinite and connexive logics ⋮ Uniform Lyndon interpolation property in propositional modal logics ⋮ An interpolating theorem prover ⋮ Toward a theory of the process of explanation ⋮ Intuitionistic logic and implicit definability ⋮ How QBF expansion makes strategy extraction hard ⋮ Restricted interpolation over modal logic S4 ⋮ On interpolation in automated theorem proving ⋮ On a generalized modularization theorem
Cites Work
This page was built for publication: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
