Re: [isabelle] z3 proof reconstruction failure
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.
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
> So is there an easy way (e.g., by declaring a z3_rule) of making
> proof reconstruction succeed in my example?
> Am 18.07.2011 12:25, schrieb Sascha Boehme:
> >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)
> >Matthias Schmalz wrote:
> >>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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and