Re: [isabelle] Blast behaves strangely with free schematic variables

Schematic variables can be replaced by any well-formed term, and there are no guarantees that this will be done in an elegant or minimal way. You get the first proof that was found. It would be nice if blast allowed backtracking over different proofs, but to obtain reasonable performance it's necessary to prune the search space.

Larry Paulson

On 18 Feb 2006, at 15:07, Tim Freeman wrote:

   lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n

I had expected it to say:

   lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY

I was surprised by the intruction of the "gcd" operator. If I change
"blast" to "auto", I do get the output I expected.

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