On interpolation in automated theorem proving

DOI10.1007/s10817-014-9314-0zbMath1315.03018OpenAlexW2064300892MaRDI QIDQ2352502

Maria Paola Bonacina, Moa Johansson

Publication date: 2 July 2015

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

Full work available at URL: https://doi.org/10.1007/s10817-014-9314-0

zbMATH Keywords

superpositionresolutioninterpolation systems

Mathematics Subject Classification ID

Related Items (6)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Craig interpolation with clausal first-order tableaux ⋮ On First-Order Model-Based Reasoning ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Unnamed Item ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Uses Software

• VAMPIRE
• SPASS
• z3
• SIMPLIFY
• E Theorem Prover
• FOCI
• Wolverine

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interpolation systems for ground proofs in automated deduction: a survey
• On deciding satisfiability by theorem proving with speculative inferences
• Methods of cut-elimination
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Modal languages and bounded fragments of predicate logic
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• On the mechanical derivation of loop invariants
• A rewriting approach to satisfiability procedures.
• Superposition as a decision procedure for timed automata
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• An interpolating theorem prover
• Model-based Theory Combination
• Rewrite-Based Satisfiability Procedures for Recursive Data Structures
• System Description: E 1.8
• From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
• Playing in the grey area of proofs
• Efficient generation of craig interpolants in satisfiability modulo theories
• On Interpolation in Decision Procedures
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Solving SAT and SAT Modulo Theories
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Interpolant Strength
• Simplification by Cooperating Decision Procedures
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Ground Interpolation for Combined Theories
• Interpolation and Symbol Elimination
• Heaps and Data Structures: A Challenge for Automated Provers
• Automated deduction for verification
• New results on rewrite-based satisfiability procedures
• Quantifier-free interpolation in combinations of equality interpolating theories
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Interpolation and Symbol Elimination in Vampire
• Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
• Computer Aided Verification

This page was built for publication: On interpolation in automated theorem proving