Unification with abstraction and theory instantiation in saturation-based reasoning

DOI10.1007/978-3-319-89960-2_1MaRDI QIDQ2324203zbMATH OpenOpenAlexFDO

Authors Giles Reger, Martin Suda, 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

Recommendations

• Making theory reasoning simpler
• Schematic saturation for decision and unification problems.
• Theory Instantiation
• Engineering DPLL(T) + Saturation
• SMELS: Satisfiability Modulo Equality with Lazy Superposition

Cited in

(18)

• Towards satisfiability modulo parametric bit-vectors
• A combinator-based superposition calculus for higher-order logic
• Layered clause selection for theory reasoning (short paper)
• Making theory reasoning simpler
• Towards bit-width-independent proofs in SMT solvers
• SAT Encoding of Unification in $\mathcal{EL}$
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• Superposition with Delayed Unification
• Program Synthesis in Saturation
• ALASCA: reasoning in quantified linear arithmetic
• Difference of constrained patterns in logically constrained term rewrite systems
• Partial redundancy in saturation
• SMT and functional equation solving over the reals: challenges from the IMO
• Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
• Automating induction by reflection
• Refining unification with abstraction
• Reducibility constraints in superposition
• A higher-order Vampire (short paper)

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324203)