Re: [isabelle] SMT integration to Isabelle/HOL



Am 16.04.2012 um 13:13 schrieb Christian Sternagel:

> Just a remark: I'm pretty sure that Isabelle/HOL does not use oracles to
> integrate SMT solvers.

Actually, it allows both. If you add

    declare [[smt_oracle = true]]

then from then on proofs found by SMT solvers (and parts of the translation from HOL to the SMT-LIB syntax) will be trusted. This is, of course, very dangerous; indeed, I was able to prove "False" on one occasion thanks to a bug in Yices.

Sascha might have more to say about the orignal question by Shuling Wang, but in short the SMT architecture is quite flexible; the files "HOL/Tools/SMT/smt_setup_solvers.ML" and "HOL/Tools/SMT/smt_solver.ML" show how it's done.

Jasmin






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