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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and