Interpolation and Symbol Elimination

DOI10.1007/978-3-642-02959-2_17zbMath1250.68193MaRDI 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

68Q60: Specification and verification (program logics, model checking, etc.)

03B35: Mechanization of proofs and logical operations

03C40: Interpolation, preservation, definability

Related Items

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

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