[isabelle] Announcement: ismt: Connecting Isabelle/HOL and Yices SMT solver
Galois, Inc. is pleased to announce the release of ismt (v1.2). The
ismt package allows Isabelle to invoke SRI Inc.'s Yices SMT solver to
automatically prove or refute HOL formulas. When Yices refutes a
formula, the ismt package can also convert the Yices-produced
counterexample back into a higher order logic formula. The ismt
package and documentation can be downloaded from:
Note that ismt is an external oracle. While we have tried to ensure
ismt is sound, there is always the possibility that ismt contains
logical errors that won't be caught by Isabelle. Use at your own risk.
We welcome any questions, comments, and feature requests.
Levent Erkok (levent.erkok at galois.com)
John Matthews (matthews at galois.com)
This archive was generated by a fusion of
Pipermail (Mailman edition) and