Re: [isabelle] confusing metis message



The message should be the truth when you have given metis all of HOL. But since one tends to be a bit more selective, I agree that it is confusing.

Now I'm more confused - here it seems that it failed due to not
expanding Domain and Range, and so (even given all of HOL) would
similarly fail,

My "all of HOL" was meant to include all your definitions.

But, in any case, your remark suggests I've misunderstood what a
typical invocation would be, or what it already knows?

Metis knows first-order logic. Everything else you have to tell it. In contrast to blast. Hence metis is primarily useful in connection with sledgehammer, which figures out the required lemmas for you.

Tobias





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