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