Re: [isabelle] Schematic vars or universal bound vars in theorem?

On 7/22/2012 10:57 AM, Gottfried Barrow wrote:
To make a long story short, if I give Sledgehammer a theorem that's only
HOL, and HOL is consistent, then Sledgehammer can only prove that the
theorem is true or that its negation is false.

I read my emails over and over again before I send them out, but I still end up having to clutter up the list with two emails instead of one to clarify something.

Sledgehammer proves things true. Nitpick proves things false. Like I said, negative logic can mess me up in the most simple ways.

Explicitly correcting what I said, if a logic is consistent, then Sledgehammer can prove a theorem true or proves its negation true, but not both.


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