Re: [isabelle] z3 proof reconstruction failure

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?


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:
     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 MHonArc.