Using Yices as an Automated Solver in Isabelle/HOL
Levent Erkök and John Matthews
Appears in AFM '08
We describe our integration of the Yices SMT solver into
the Isabelle theorem prover. This integration allows users
to take advantage of the powerful SMT solving techniques
within the interactive theorem proving environment of Isabelle,
considerably increasing the automation level for a
significant subset of Isabelle/HOL.