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