Interpolation and Symbol Elimination in Vampire

DOI10.1007/978-3-642-14203-1_16zbMath1291.68348OpenAlexW1744405537MaRDI QIDQ5747760

Laura Kovács, Andrei Voronkov, Kryštof Hoder

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_16

Mathematics Subject Classification ID

Related Items

Interpolation systems for ground proofs in automated deduction: a survey, Symbol elimination and applications to parametric entailment problems, Complete instantiation-based interpolation, An extension of lazy abstraction with interpolation for programs with arrays, On Interpolation in Decision Procedures, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Sine Qua Non for Large Theory Reasoning, On Interpolation and Symbol Elimination in Theory Extensions, Predicate Elimination for Preprocessing in First-Order Theorem Proving, On invariant synthesis for parametric systems, On interpolation in automated theorem proving

Uses Software

• VAMPIRE
• TPTP
• z3

Cites Work

• Unnamed Item
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Abstractions from proofs
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• System Description: Spass Version 3.0
• Interpolation and Symbol Elimination
• A framework for numeric analysis of array operations
• Automated Deduction – CADE-20
• Array Abstractions from Proofs
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification