Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
From MaRDI portal
Publication:3244103
Cites work
Cited in
(only showing first 100 items - show all)- Ground Interpolation for the Theory of Equality
- Joint consistency in extensions of the minimal logic
- Hybrid extensions of the minimal logic
- Interpolation and definability over the logic Gl
- Interpolation-based GR(1) assumptions refinement
- Decidability of the weak interpolation property over the minimal logic
- Interpolation and the projective Beth property in well-composed logics
- Differentiable learning of matricized DNFs and its application to Boolean networks
- Through an inference rule, darkly
- Algorithmic introduction of quantified cuts
- Causality-based game solving
- Interpolation and model checking for nonlinear arithmetic
- Semantic interpolation
- Failure of interpolation in combined modal logics
- The institution-theoretic scope of logic theorems
- Resolution proof transformation for compression and interpolation
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Nondeterministic functions and the existence of optimal proof systems
- Beth definability, interpolation and language splitting
- The metatheory of the classical propositional calculus is not axiomatizable
- Linear reasoning in modal logic
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- On propositional definability
- Whale: an interpolation-based algorithm for inter-procedural verification
- Intuitionistic logic and implicit definability
- Abstract Counterexamples for Non-disjunctive Abstractions
- Some applications of propositional logic to cellular automata
- Recognizability of all WIP-minimal logics
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Exploiting partial variable assignment in interpolation-based model checking
- The interpolation problem in finite-layered pre-Heyting logics
- Common knowledge does not have the Beth property
- Algorithms for recognizing restricted interpolation over the modal logic S4
- Interpolation and amalgamation for arrays with MaxDiff
- Farkas-based tree interpolation
- The road to two theorems of logic
- Proof tree preserving tree interpolation
- Lattice-based refinement in bounded model checking
- On interpolation problem in paraconsistent extensions of the minimal logic
- Interpolation and Symbol Elimination
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- The decidability of Craig's interpolation property in well-composed J-logics
- Horn clause solvers for program verification
- Proof complexity of non-classical logics
- An extension of lazy abstraction with interpolation for programs with arrays
- Maksimova, relevance and the study of lattices of non-classical logics
- Quantifier-free interpolation in combinations of equality interpolating theories
- Perceptibility in pre-Heyting logics
- 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\)
- 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
- Interpolation in weakly transitive modal logics
- Craig Interpolation for Linear Temporal Languages
- scientific article; zbMATH DE number 3259043 (Why is no real title available?)
- On Languages Which are Based on Non-Standard Arithmetic
- Toward a theory of the process of explanation
- Craig interpolation in the presence of unreliable connectives
- 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
- Generalized interpolation theorems
- Complete instantiation-based interpolation
- On enumerating query plans using analytic tableau
- How QBF expansion makes strategy extraction hard
- Harmonious logic: Craig's interpolation theorem and its descendants
- On dynamically generated ontology translators in agent communication
- SMT-based verification of program changes through summary repair
- Effective interpolation and preservation in guarded logics
- Partition-based logical reasoning for first-order and propositional theories
- SOME MODEL THEORY OF GUARDED NEGATION
- Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras
- On a generalized modularization theorem
- On interpolation when function symbols are present
- Optimization techniques for Craig interpolant compaction in unbounded model checking
- Minding the is-ought gap
- Amalgamation, interpolation, and implicit definability in varieties of algebras
- The logic of secrets and the interpolation rule
- Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
- Rewriting interpolants
- The Lyndon property and uniform interpolation over the Grzegorczyk logic
- The Craig interpolation theorem in abstract model theory
- Modularity results for interpolation, amalgamation and superamalgamation
- scientific article; zbMATH DE number 7566058 (Why is no real title available?)
- From choosing elements to choosing concepts: the evolution of Feferman's work in model theory
- Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys
- Interpolation theorems in modal logics. Sufficient conditions
- 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
- Interpolation in extensions of first-order logic
- Der Interpolationssatz der intuitionistischen Prädikatenlogik
- Refining abstract interpretations
- Craig interpolation with clausal first-order tableaux
- Satisfiability modulo theories
- Definability for model counting
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)
