[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.

Happy proving,

Levent Erkok (levent.erkok at galois.com)
John Matthews (matthews at galois.com)

Galois, Inc.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.