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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and