Interpolation and Symbol Elimination

DOI10.1007/978-3-642-02959-2_17zbMath1250.68193OpenAlexW1515795741MaRDI QIDQ5191103

Laura Kovács, Andrei Voronkov

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_17

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Related Items

Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Symbol elimination and applications to parametric entailment problems ⋮ Interpolation and Model Checking ⋮ Constraint solving for interpolation ⋮ On Interpolation in Decision Procedures ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ On Transfinite Knuth-Bendix Orders ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Model completeness, covers and superposition ⋮ NIL: learning nonlinear interpolants ⋮ On invariant synthesis for parametric systems ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ On interpolation in automated theorem proving

Uses Software

• VAMPIRE
• FOCI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An interpolation theorem in the predicate calculus
• Decision procedures for extensions of the theory of arrays
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Abstractions from proofs
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
• Integrating Linear Arithmetic into Superposition Calculus
• Interpolation in Local Theory Extensions
• Equality and lyndon's interpolation theorem
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Cover Algorithms and Their Combination
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification