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.