Hi Bill,
>Freek's miz3 code in the miz3 dox 1201.3601-1.pdf
>solving the drinker's paradox on p 13--14 is perhaps designed to show
>various features of miz3, but it is more than twice as long as needed:
It's mainly intended to be as close as possible to the
Jaśkowsky/Fitch-style natural deduction proof that's right
before it, to show off the similarity of the proof styles.
That one you _can't_ make significantly shorter, because only
the basic natural deduction intro and elim rules are allowed.
But if you want to be short, then
let DRINKER = thm `;
let P be A->bool;
thus ?x. P x ==> !y. P y`;;
already works. Getting a short proof, or even a proof
that mimics how a human would understand this, was not
the primary aim of the example. And yes, showing off the
various miz3 proof steps _was_ one of its aims.
If you like to see a _really_ involved proof of this
statement, then look at
http://www.cs.ru.nl/~freek/notes/drinker.miz
Now that's a silly version, as Mizar also can prove this
without any help. But this one would also work in a minimal
logic version of Mizar :-)
Freek
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
