Email Gateway (Aug 18 2022 at 19:34): Email Gateway (Aug 18 2022 at 19:34):From: Shuling Wang <wangsl@ios.ac.cn>
Hello,
We are trying to integrate an SMT solver to Isabelle/HOL. It seems that the
integration of external procedures is done by defining oracles in Isabelle.
I see that the new release of Isabelle supports SMT solvers like Z3, CVC,
Yices. I would like to know that, if we implement the SMT solver in the same
language as Z3, and also the same input standard, can we avoid defining the
oracle and apply the existing oracle for Z3 directly?
I find that our use of Isabelle/HOL needs to go to the ML level, e.g.,
defining tactics, and SMT integration mentioned above. But it is very
difficult for me to understand the ML implemental theories of Isabelle/HOL.
Can you please give me some directions to learn them, or any documents
especially about the oracle and tactics faculties of Isabelle?
Looking forward to your reply. Thanks.
Best,
Wang Shuling
Institute of Software
Chinese Academy of Sciences
Best,
王淑灵 Wang Shuling
Institute of Software
Chinese Academy of Sciences
Email Gateway (Aug 18 2022 at 19:34):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Just a remark: I'm pretty sure that Isabelle/HOL does not use oracles to
integrate SMT solvers. The reason is that this would mean to base
Isabelle/HOL's correctness on the correctness of external tools (which
does not fit the usual "small trusted kernel" philosophy). The
integration has to be roughly of the following shape:
Isabelle asks an SMT solver to give a proof for some statement.
The SMT solvers tries to do so, and if successful gives a certificate of
some form.
Isabelle reads back this certificate using a verified routine (i.e.,
logical inferences go through the trusted kernel) and if successful
accepts the result.
E.g., in the case of sledgehammer (which integrates first-order provers
into Isabelle) the certification mechanism is to replay the found proof
using a fully verified (i.e., "written in Isabelle") first-order prover.
(I am a bit sloppy about the details, but I guess the general picture is
correct.)
cheers
chris
Email Gateway (Aug 18 2022 at 19:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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
Email Gateway (Aug 18 2022 at 19:34):From: Tobias Nipkow <nipkow@in.tum.de>
Am 16/04/2012 05:54, schrieb Shuling Wang:
Hello,
We are trying to integrate an SMT solver to Isabelle/HOL. It seems that the
integration of external procedures is done by defining oracles in Isabelle.
I see that the new release of Isabelle supports SMT solvers like Z3, CVC,
Yices. I would like to know that, if we implement the SMT solver in the same
language as Z3, and also the same input standard, can we avoid defining the
oracle and apply the existing oracle for Z3 directly?
You can share Isabelle's Z3 oracle if your input language is the same as Z3.
Jasmin already pointed you to the relevant files.
The Z3 link can also reconstruct Z3 proofs in Isabelle (thanks to Sascha), which
is the safest way to integrate extertnal tools. If your SMT solver outputs
proofs in the Z3 format, Isabelle could check them, too.
Tobias
I find that our use of Isabelle/HOL needs to go to the ML level, e.g.,
defining tactics, and SMT integration mentioned above. But it is very
difficult for me to understand the ML implemental theories of Isabelle/HOL.
Can you please give me some directions to learn them, or any documents
especially about the oracle and tactics faculties of Isabelle?Looking forward to your reply. Thanks.
Best,
Wang Shuling
Institute of Software
Chinese Academy of Sciences
Best,
王淑灵 Wang Shuling
Institute of Software
Chinese Academy of Sciences
Email Gateway (Aug 18 2022 at 19:34):From: Makarius <makarius@sketis.net>
On Mon, 16 Apr 2012, Shuling Wang wrote:
I find that our use of Isabelle/HOL needs to go to the ML level, e.g.,
defining tactics, and SMT integration mentioned above. But it is very
difficult for me to understand the ML implemental theories of
Isabelle/HOL.
The ML tools of Isabelle/HOL are indeed quite complex, but this does not
mean that one should be afraid of Isabelle/ML in general. Isabelle/Isar
and Isabelle/ML are tightly integrated, and I usually do not speak of a
separate "ML level". It is more like the Yin and Yang (阴阳) of Isabelle.
Can you please give me some directions to learn them, or any documents
especially about the oracle and tactics faculties of Isabelle?
The isar-ref manual section 5.11 explains oracles and points to some basic
example in ~~/src/HOL/ex/Iff_Oracle.thy which can be taken as a starting
point to warm-up with Isabelle/ML and Isabelle/Isar intermixed.
This is best used with the Isabelle/jEdit Prover IDE. I.e. you start
"isabelle jedit" and open the Iff_Oracle.thy file. ML that is directly
embedded into theory sources is marked up with inferred type information
and hyperlinks for identifiers in the ML text. This greatly helps to
navigate ML sources, but it does not work yet for external ML files.
Makarius
Email Gateway (Aug 18 2022 at 19:34):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
A word of warning: the Z3 link can reconstruct Z3 proofs, but Sascha had
to do a lot of guesswork. Z3 breaks large proofs down into component
steps, which is very helpful. Some of these steps are still very large,
however, and all that is given is a name (such as "lemma" or "rewrite").
Sascha guessed what Z3 had done and picked appropriate Isabelle tools,
which might be totally inappropriate for your tool.
In conclusion: Z3's proof output format is far from ideal. You might be
able to come up with a much better one yourself. I can give you some
hints at a later point. Also, the Z3 input language Sascha picked is
just SMTLIB/SMTLIB2.
I would recommend you start by reading some of Sascha's papers on his
work. See http://www4.in.tum.de/~boehmes/ (especially "Fast LCF-style
Proof Reconstruction for Z3").
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 19:34):From: wangsl@ios.ac.cn
Thanks so much for all your very helpful answers. I realise that it is
very necessary to understand the Isabelle/ML for my use of Isabelle. It is
indeed very tightly integrated to Isabelle/Isar. The literatures and
papers you advised are very helpful for me.
We have just started to implement an SMT solver mainly for reasoning about
polynomial arithmetic based on the previous work of my colleagues. This
SMT solver will be a backend prover for our theorem proving HCSP
(continuous + CSP) programs in Isabelle. So we consider at first picking a
unified input language and output language for it, like SMTLIB standard,
and thus may save some effort when integrating it to Isabelle. But we will
now consider this more carefully for the sake of later reconstruction
proof in Isabelle.
Thanks again.
Best,
Shuling
Email Gateway (Aug 18 2022 at 19:35):From: wangsl@ios.ac.cn
Send Cl-isabelle-users mailing list submissions to
cl-isabelle-users@lists.cam.ac.ukTo subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
cl-isabelle-users-request@lists.cam.ac.ukYou can reach the person managing the list at
cl-isabelle-users-owner@lists.cam.ac.ukWhen replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."Today's Topics:
1. Re: SMT integration to Isabelle/HOL (Thomas Sewell)
Message: 1
Date: Tue, 17 Apr 2012 12:23:29 +1000
From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Subject: Re: [isabelle] SMT integration to Isabelle/HOL
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <4F8CD421.4090305@nicta.com.au>
Content-Type: text/plain; charset=GB2312On 16/04/12 22:00, Tobias Nipkow wrote:
Am 16/04/2012 05:54, schrieb Shuling Wang:
Hello,
We are trying to integrate an SMT solver to Isabelle/HOL. It seems that
the
integration of external procedures is done by defining oracles in
Isabelle.
I see that the new release of Isabelle supports SMT solvers like Z3,
CVC,
Yices. I would like to know that, if we implement the SMT solver in the
same
language as Z3, and also the same input standard, can we avoid defining
the
oracle and apply the existing oracle for Z3 directly?
You can share Isabelle's Z3 oracle if your input language is the same as
Z3.
Jasmin already pointed you to the relevant files.The Z3 link can also reconstruct Z3 proofs in Isabelle (thanks to
Sascha), which
is the safest way to integrate extertnal tools. If your SMT solver
outputs
proofs in the Z3 format, Isabelle could check them, too.Tobias
A word of warning: the Z3 link can reconstruct Z3 proofs, but Sascha had
to do a lot of guesswork. Z3 breaks large proofs down into component
steps, which is very helpful. Some of these steps are still very large,
however, and all that is given is a name (such as "lemma" or "rewrite").
Sascha guessed what Z3 had done and picked appropriate Isabelle tools,
which might be totally inappropriate for your tool.In conclusion: Z3's proof output format is far from ideal. You might be
able to come up with a much better one yourself. I can give you some
hints at a later point. Also, the Z3 input language Sascha picked is
just SMTLIB/SMTLIB2.I would recommend you start by reading some of Sascha's papers on his
work. See http://www4.in.tum.de/~boehmes/ (especially "Fast LCF-style
Proof Reconstruction for Z3").Thank you for providing the references. Very helpful.
Yours,
Thomas.End of Cl-isabelle-users Digest, Vol 82, Issue 20
Email Gateway (Aug 18 2022 at 19:35):From: Chantal KELLER <chantal.keller@wanadoo.fr>
Hello Shuling,
I want to point to you that there is a proposal for a unified output
language for SMT solver that has been proved to be easy to integrate to
interactive theorem provers:
<http://www.loria.fr/~fontaine/Besson1.pdf>. See
<http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html> for an
integration of such an output in Coq.
Cheers,
Chantal.
Last updated: Apr 23 2024 at 08:19 UTC