Interpolation and Symbol Elimination
From MaRDI portal
Publication:5191103
DOI10.1007/978-3-642-02959-2_17zbMath1250.68193MaRDI QIDQ5191103
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
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, Parallelizing SMT solving: lazy decomposition and conciliation, 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
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
