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 (12)

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

This page was built for publication: Interpolation and Symbol Elimination in Vampire