Re: [isabelle] refute refutes my simple axiom

Hi Gottfried,

> Refute is finding a model. I simplified everything down to a theorem which states a simple axiom as an exists instead of a forall, and refute finds a model, although metis proves the theorem. I don't know how to interpret the results of refute. Here's the theory.

Refute is unsound in the presence of axioms, because it will fail to pick these up. For cases like these, you have to use Nitpick.

As a general rule, Nitpick subsumes Refute and there is no reason to use the latter. Refute is provided for historical reasons and might disappear in a future release.



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