Re: [isabelle] SMT integration to Isabelle/HOL



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
> Send Cl-isabelle-users mailing list submissions to
> 	cl-isabelle-users at lists.cam.ac.uk
>
> To 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 at lists.cam.ac.uk
>
> You can reach the person managing the list at
> 	cl-isabelle-users-owner at lists.cam.ac.uk
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Cl-isabelle-users digest..."
>
>
> Today's Topics:
>
>    1.  SMT integration to Isabelle/HOL (Shuling Wang)
>    2. Re:  SMT integration to Isabelle/HOL (Christian Sternagel)
>    3. Re:  SMT integration to Isabelle/HOL (Jasmin Blanchette)
>    4. Re:  SMT integration to Isabelle/HOL (Tobias Nipkow)
>    5. Re:  SMT integration to Isabelle/HOL (Makarius)
>    6.  Thedu: 2nd Call for papers (Makarius)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 16 Apr 2012 11:54:22 +0800
> From: "Shuling Wang" <wangsl at ios.ac.cn>
> Subject: [isabelle] SMT integration to Isabelle/HOL
> To: <cl-isabelle-users at lists.cam.ac.uk>
> Message-ID: <002501cd1b84$9c19c520$d44d4f60$ at ac.cn>
> Content-Type: text/plain;	charset="gb2312"
>
> 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
>
>
>
>
>
> ------------------------------
>
> Message: 2
> Date: Mon, 16 Apr 2012 20:13:51 +0900
> From: Christian Sternagel <c-sterna at jaist.ac.jp>
> Subject: Re: [isabelle] SMT integration to Isabelle/HOL
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <4F8BFEEF.2020900 at jaist.ac.jp>
> Content-Type: text/plain; charset=GB2312
>
> 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
>
> On 04/16/2012 12:54 PM, Shuling Wang wrote:
>> 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
>>
>>
>>
>
>
>
>
> ------------------------------
>
> Message: 3
> Date: Mon, 16 Apr 2012 13:33:43 +0200
> From: Jasmin Blanchette <jasmin.blanchette at gmail.com>
> Subject: Re: [isabelle] SMT integration to Isabelle/HOL
> To: Christian Sternagel <c-sterna at jaist.ac.jp>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <09A03F6A-26EE-49F6-A98B-FA420F50A8A2 at gmail.com>
> Content-Type: text/plain; charset=us-ascii
>
> 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
>
>
>
>
> ------------------------------
>
> Message: 4
> Date: Mon, 16 Apr 2012 14:00:21 +0200
> From: Tobias Nipkow <nipkow at in.tum.de>
> Subject: Re: [isabelle] SMT integration to Isabelle/HOL
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <4F8C09D5.3030902 at in.tum.de>
> Content-Type: text/plain; charset=GB2312
>
> 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
>>
>>
>
>
>
> ------------------------------
>
> Message: 5
> Date: Mon, 16 Apr 2012 15:33:17 +0200 (CEST)
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] SMT integration to Isabelle/HOL
> To: Shuling Wang <wangsl at ios.ac.cn>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Message-ID:
> 	<alpine.LNX.2.00.1204161524510.31391 at macbroy21.informatik.tu-muenchen.de>
>
> Content-Type: text/plain; charset="gb2312"
>
> 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
>
> ------------------------------
>
> Message: 6
> Date: Mon, 16 Apr 2012 20:43:19 +0200 (CEST)
> From: Makarius <makarius at sketis.net>
> Subject: [isabelle] Thedu: 2nd Call for papers
> To: isabelle-users at cl.cam.ac.uk
> Message-ID:
> 	<alpine.LNX.2.00.1204162043020.6576 at macbroy21.informatik.tu-muenchen.de>
>
> Content-Type: text/plain; charset="utf-8"
>
> ----------------------------------------------------------------------
>                            2nd CALL FOR PAPERS
> ----------------------------------------------------------------------
>                                THedu'12
>                   TP components for educational software
>                               11 July 2012
>                 http://www.uc.pt/en/congressos/thedu/thedu12
>
>                              Workshop at CICM 2012
>                  Conferences on Intelligent Computer Mathematics
>                                9-14 July 2012
>                     Jacobs University, Bremen, Germany
>              http://www.informatik.uni-bremen.de/cicm2012/cicm.php
>
> ----------------------------------------------------------------------
>
> THedu'12 Scope
> --------------
>
> This workshop intends to gather the research communities for computer
> Theorem proving (TP), Automated Theorem Proving (ATP), Interactive
> Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS)
> and Dynamic Geometry Systems (DGS). The workshop tries to combine and
> focus systems of these areas to enhance existing educational software
> as well as studying the design of the next generation of mechanised
> mathematics assistants (MMA). Elements for next-generation MMA's
> include:
>
>      * Declarative Languages for Problem Solution: education in applied
>        sciences and in engineering is mainly concerned with problems,
>        which involve operations on elementary objects to be transformed
>        to an object representing a problem solution. Preconditions and
>        postconditions of these operations can be used to describe the
>        possible steps in the problem space; thus, ATP-systems can be used
>        to check if an operation sequence given by the user does actually
>        present a problem solution. Such "Problem Solution Languages"
>        encompass declarative proof languages like Isabelle/Isar or Coq's
>        Mathematical Proof Language, but also more specialized forms such
>        as, for example, geometric problem solution languages that express
>        a proof argument in Euclidian Geometry or languages for graph
>        theory.
>
>      * Consistent Mathematical Content Representation: Libraries of
>        existing ITP-Systems, in particular those following the LCF-prover
>        paradigm, usually provide logically coherent and human readable
>        knowledge. In the leading provers, mathematical knowledge is
>        covered to an extent beyond most courses in applied
>        sciences. However, the potential of this mechanised knowledge for
>        education is clearly not yet recognised adequately: renewed
>        pedagogy calls for inquiry-based learning from concrete to
>        abstract --- and the knowledge's logical coherence supports such
>        learning: for instance, the formula 2.pi depends on the definition
>        of reals and of multiplication; close to these definitions are the
>        laws like commutativity etc. However, the complexity of the
>        knowledge's traceable interrelations poses a challenge to
>        usability design.
>
>      * User-Guidance in Stepwise Problem Solving: Such guidance is
>        indispensable for independent learning, but costly to implement so
>        far, because so many special cases need to be coded by
>        hand. However, TP technology makes automated generation of
>        user-guidance reachable: declarative languages as mentioned above,
>        novel programming languages combining computation and deduction,
>        methods for automated construction with ruler and compass from
>        specifications, etc --- all these methods 'know how to solve a
>        problem'; so, use the methods' knowledge to generate user-guidance
>        mechanically, this is an appealing challenge for ATP and ITP, and
>        probably for compiler construction!
>
> In principle, mathematical software can be conceived as models of
> mathematics: The challenge addressed by this workshop series is to
> provide appealing models for MMAs which are interactive and which
> explain themselves such that interested students can independently
> learn by inquiry and experimentation.
>
>
> Program Committee
> -----------------
>       Ralph-Johan Back, Abo Akademy University, Finland
>       Francisco Botana, University of Vigo at Pontevedra, Spain
>       Florian Haftman, Munich University of Technology, Germany
>       Predrag Janicic, University of Belgrade, Serbia
>       Cezary Kaliszyk, University of Tsukuba, Japan
>       Julien Narboux, University of Strasbourg, France
>       Filip Maric, University of Belgrade, Serbia
>       Walther Neuper, Graz University of Technology, Austria
>       Pedro Quaresma, University of Coimbra, Portugal
>       Wolfgang Schreiner, Johannes Kepler University, Linz, Austria
>       Laurent Th?ry, Sophia Antipolis, INRIA, France
>       Makarius Wenzel, University Paris-Sud, France
>       Burkhart Wolff, University Paris-Sud, France
>
>
> Important Dates (by easychair)
> ---------------
>
>       * 01 May 2012 * Extended Abstracts/Demo proposals
>       * 01 Jun 2012 * Author Notification
>       * 15 Jun 2012 * Final Version
>       * 11 Jul 2012 * Worshop Day
>       * 31 Aug 2012 * Full papers (EPTCS post-proceedings)
>
>
> Submission
> ----------
>
> We welcome submission of proposals to present a demo, as well as
> submissions of extended abstracts (5-8 pages max) presenting original
> unpublished work which is not been submitted for publication
> elsewhere.
>
> Selected extended abstracts will appear in CISUC Technical Report
> series (ISSN 0874-338X [1]). All accepted extended abstracts and
> system demos will be presented at the workshop, and the extended
> abstracts will be made available online.
>
> Extended abstracts and demo proposals should be submitted via THedu'12
> easychair [2].
>
> Extended abstracts should be 5-8 pages in length and are to be
> submitted in PDF format. They must conform to the EPTCS style
> guidelines [3].
>
> At least one author of each accepted extended abstract/demo is
> expected to attend THedu'12 and presents her or his extended
> abstract/demo.
>
> The post-proceedings (full papers, 20 pages max) will be published in
> the Electronic Proceedings in Theoretical Computer Science (EPTCS)
> series [4].
>
> ---
> [1] http://www.uc.pt/en/fctuc/ID/cisuc/RecentPublications/Techreports/
> [2] http://www.easychair.org/conferences/?conf=thedu12
> [3] http://http://style.eptcs.org/
> [4] http://eptcs.org/
>
> End of Cl-isabelle-users Digest, Vol 82, Issue 19
> *************************************************
>







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