*To*: Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch>*Subject*: Re: [isabelle] z3 proof reconstruction failure*From*: Sascha Boehme <boehmes at in.tum.de>*Date*: Mon, 18 Jul 2011 18:57:28 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4E240CB7.9000803@inf.ethz.ch>*References*: <4E23F2AC.2070203@inf.ethz.ch> <20110718102502.GA6812@lapbroy158> <4E240CB7.9000803@inf.ethz.ch>*User-agent*: Mutt/1.5.20 (2009-06-14)

Hi Matthias, It seems that declaring rules as "z3_rule" hasn't been a feature extensively tested so far. It worked only overly restricted. The next Isabelle release will be fixed in that respect. Cheers, Sascha Matthias Schmalz wrote: > Hi Sascha, > > thanks for explaining. > This is a minimal example for illustrating the problem, and I do not > really want to prove it with Z3. Yet, this kind of reconstruction > failure arises with more complicated examples, where Z3 would be > useful. > So is there an easy way (e.g., by declaring a z3_rule) of making > proof reconstruction succeed in my example? > > -Matthias > > Am 18.07.2011 12:25, schrieb Sascha Boehme: > >Hello, > > > >This is the incompleteness of proof reconstruction for Z3 in Isabelle. > >Although Z3 can find proofs for some nonlinear arithmetic problems, we > >currently do not support proof reconstruction for such proofs and > >consequently fail on them. > > > >The error message indicates some means to "complete" proof > >reconstruction in certain cases by proving intermediate steps in > >advance. I wonder, however, which rule you proved here, since the Z3 > >proof reconstruction step that failed looks nearly identical to your > >original goal. > > > >If you're willing to accept alternatives, here is one. You can prove > >the lemma by Metis: > > > > lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0" > > by (metis mult_le_0_iff) > > > >Cheers, > >Sascha > > > > > >Matthias Schmalz wrote: > >>Hello, > >> > >>when trying to proof the following (with z3): > >> > >>lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0" > >>by smt > >> > >>I get a proof reconstruction failure: > >> > >>Z3 found a proof, but proof reconstruction failed at the following subgoal: > >> assumptions: > >> x * y ≤ 0 > >> ¬ y ≤ 0 > >> ¬ x ≤ 0 > >> proposition: False > >>Adding a rule to the lemma group "z3_rule" might solve this problem. > >> > >>I tried to add an appropriate lemma to the group z3_rule, but > >>without success. Does anyone have an idea of how to make proof > >>reconstruction succeed in this case? > >> > >>-Matthias

**References**:**[isabelle] z3 proof reconstruction failure***From:*Matthias Schmalz

**Re: [isabelle] z3 proof reconstruction failure***From:*Sascha Boehme

**Re: [isabelle] z3 proof reconstruction failure***From:*Matthias Schmalz

- Previous by Date: Re: [isabelle] z3 proof reconstruction failure
- Next by Date: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Previous by Thread: Re: [isabelle] z3 proof reconstruction failure
- Next by Thread: [isabelle] Occur-Check Lemma and Unifikations-Algorithmus
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list