Unification with abstraction and theory instantiation in saturation-based reasoning

DOI10.1007/978-3-319-89960-2_1zbMath1423.68424OpenAlexW2787155581MaRDI QIDQ2324203

Martin Suda, Giles Reger, Andrei Voronkov

Publication date: 16 September 2019

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/unification-with-abstraction-and-theory-instantiation-in-saturationbased-reasoning(13ece419-3c90-4175-8ff8-f6d4a1276e60).html

Mathematics Subject Classification ID

Related Items (6)

The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Making theory reasoning simpler ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Layered clause selection for theory reasoning (short paper)

Uses Software

• VAMPIRE
• SMT-LIB
• SPASS
• z3
• SIMPLIFY
• CVC4
• Beagle
• AVATAR

This page was built for publication: Unification with abstraction and theory instantiation in saturation-based reasoning