Linear reasoning. A new form of the Herbrand-Gentzen theorem
From MaRDI portal
Publication:3249759
DOI10.2307/2963593zbMATH Open0081.24402OpenAlexW2098244894MaRDI QIDQ3249759FDOQ3249759
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/2963593
Cited In (90)
- Lower bound techniques for QBF expansion
- SAT-Based Formula Simplification
- Interpolation for extended modal languages
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Locally Boolean spectra
- A cut-free Gentzen-type system for the logic of the weak law of excluded middle
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Linear reasoning in modal logic
- The road to two theorems of logic
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Preface: Special issue on interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- Craig interpolation in the presence of non-linear constraints
- Parallelizing SMT solving: lazy decomposition and conciliation
- Predicate abstraction for program verification
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Guiding Craig interpolation with domain-specific abstractions
- Properties preserved under algebraic constructions
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- An institution-independent proof of the Robinson consistency theorem
- Experience of improving the BLAST static verification tool
- On recursion-free Horn clauses and Craig interpolation
- The relevance of premises to conclusions of core proofs
- Alternative semantics for unawareness
- Persistent and invariant formulas relative to theories of higher order
- Approximation Refinement for Interpolation-Based Model Checking
- A simple algebraic proof of the equational interpolation theorem
- Incremental preprocessing methods for use in BMC
- A semantic approach to interpolation
- Harmonious logic: Craig's interpolation theorem and its descendants
- Interpolation in computing science: The semantics of modularization
- The many faces of interpolation
- Partition-based logical reasoning for first-order and propositional theories
- Constraint solving for interpolation
- On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic
- Expansion-based QBF solving versus Q-resolution
- Efficient generation of small interpolants in CNF
- A Lemma which Distinguishes Minimal Logics from Other Logics
- Interpolation in Grothendieck institutions
- The Craig interpolation theorem in abstract model theory
- Title not available (Why is that?)
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Der Interpolationssatz der intuitionistischen Prädikatenlogik
- Title not available (Why is that?)
- Preservation of Craig interpolation by the product of matrix logics
- Multicomponent proof-theoretic method for proving interpolation properties
- Refinements of Vaught's normal from theorem
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- A layered algorithm for quantifier elimination from linear modular constraints
- Interpolation theorems for intuitionistic predicate logic
- On interpolation in automated theorem proving
- A compact representation of proofs
- LOGICALITY AND MODEL CLASSES
- Combining model checking and data-flow analysis
- On sequence-conclusion natural deduction systems
- A unifying view on SMT-based software verification
- Amalgamation, congruence-extension, and interpolation properties in algebras
- Parallel interpolation, splitting, and relevance in belief change
- Mixed-valued predicate calculi
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Failure tabled constraint logic programming by interpolation
- An extension of the Craig-Lyndon interpolation theorem
- Interpolant learning and reuse in SAT-based model checking
- Through an inference rule, darkly
- Annual Meeting of the Association for Symbolic Logic
- Reasoning in the theory of heap: satisfiability and interpolation
- Interpolation and model checking
- Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
- NIL: learning nonlinear interpolants
- Software verification with PDR: an implementation of the state of the art
- Craig interpolation in the presence of unreliable connectives
- Generalized Craig interpolation for stochastic Boolean satisfiability problems
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- On interpolation when function symbols are present
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- 2006–07 Winter Meeting of the Association for Symbolic Logic
- From choosing elements to choosing concepts: the evolution of Feferman's work in model theory
- Craig interpolation with clausal first-order tableaux
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Special cases of the interpolation theorem for classical predicate calculus
- Partial predicate abstraction and counter-example guided refinement
- On a Characteristic Feature of the Positive Logics
- Range-restricted and Horn interpolation through clausal tableaux
- Title not available (Why is that?)
- Designing protocols for abductive hypothesis refinement in dynamic multiagent environments
- MAXIMALITY OF LOGIC WITHOUT IDENTITY
- Definibility in normal theories
This page was built for publication: Linear reasoning. A new form of the Herbrand-Gentzen theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3249759)
