Re: [isabelle] z3 proof reconstruction failure



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





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