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)
Effective Interpolation and Preservation in Guarded Logics ⋮ Progression of Decomposed Local-Effect Action Theories ⋮ On Languages Which are Based on Non-Standard Arithmetic ⋮ Interpolation Method for Multicomponent Sequent Calculi ⋮ Complexity of interpolation and related problems in positive calculi ⋮ Linear reasoning in modal logic ⋮ Satisfaction for n-th order languages defined in n-th order languages ⋮ On Automorphisms of Polyadic Algebras ⋮ Lower bounds to the size of constant-depth propositional proofs ⋮ The metatheory of the classical propositional calculus is not axiomatizable ⋮ ABSTRACT FORMS OF QUANTIFICATION IN THE QUANTIFIED ARGUMENT CALCULUS ⋮ SMT-based verification of program changes through summary repair ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ 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 ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ The logic of secrets and the interpolation rule ⋮ Differentiable learning of matricized DNFs and its application to Boolean networks ⋮ Craig's interpolation property in pretabular logics ⋮ Eine Semantische Charakterisierung der Durch die Implikation Allein Darstellbaren Wahrheitsfunktionen ⋮ A proof theoretic proof of Scott's general interpolation theorem ⋮ Unnamed Item ⋮ Generalized interpolation theorems ⋮ Complete instantiation-based interpolation ⋮ Interpolants for Linear Arithmetic in SMT ⋮ Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic ⋮ Lower bounds for resolution and cutting plane proofs and monotone computations ⋮ SOME MODEL THEORY OF GUARDED NEGATION ⋮ On interpolation when function symbols are present ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Rewriting Interpolants ⋮ On Interpolation Problem in Paraconsistent Extensions of the Minimal Logic ⋮ Parallel interpolation, splitting, and relevance in belief change ⋮ Failure of interpolation in combined modal logics ⋮ Interpolation and Symbol Elimination ⋮ Unnamed Item ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints ⋮ Ground Interpolation for the Theory of Equality ⋮ Maksimova, Relevance and the Study of Lattices of Non-classical Logics ⋮ Decidability of Some Interpolation Properties for Weakly Transitive Modal Logics ⋮ From Choosing Elements to Choosing Concepts: The Evolution of Feferman’s Work in Model Theory ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ Proof Complexity of Non-classical Logics ⋮ Craig Interpolation for Linear Temporal Languages ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Some applications of propositional logic to cellular automata ⋮ Temporal logics of “the next” do not have the beth property ⋮ 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
Cites Work
This page was built for publication: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
