# Re: [isabelle] refute refutes my simple axiom

On Tue, 2012-07-17 at 15:19 -0500, Gottfried Barrow wrote:
> 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 simply disregards user-supplied axioms (other than type and
constant definitions). See Section 3.4 (page 52) of
http://user.it.uu.se/~tjawe125/publications/weber08satbased.html
for a brief discussion. As you noticed, this may well lead to spurious
(counter-)models in the presence of such axioms.
I suggest that you use nitpick instead, which -- for all practical
intents and purposes -- is a worthy successor to refute.
Best regards,
Tjark

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