Email Gateway (Aug 18 2022 at 12:18): Email Gateway (Aug 18 2022 at 12:18):From: Levent Erkok <levent.erkok@galois.com>
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:
http://www.galois.com/company/open_source/ismt
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@galois.com)
John Matthews (matthews@galois.com)
Galois, Inc.
Last updated: May 03 2024 at 04:19 UTC