Hi Bill,
On Fri, Jul 20, 2012 at 12:00 PM, Bill Richter <
[email protected]> wrote:
> Thanks, Cris, I did not know about John's paper
> http://www.cl.cam.ac.uk/~jrh13/papers/me.html. It looks very
> interesting, but his interesting details aren't what what I want to talk
> about. I want to know if my education ideas fall apart if e.g. we put no
> `limit on depth of chaining.' Otherwise we're talking about Michael's
> heuristics, where you fiddle with various parameters trying to `hit the
> sweet spot' where tedious things are proven easily and astounding results
> don't get proven automatically. I'm satisfied that experts like John &
> Freek have done a great job with the heuristics. I'm not going to try to
> explain that to my audience of mathematicians, even if I understood it
> myself. I'm looking for some kind of upper bound on how astounding a
> result you can prove with little work if we have no heuristics, e.g. no
> `limit on depth of chaining.'
>
Do your education ideas fall apart if e.g. we put no 'limit on depth of
chaining'; in other words can proof steps tend to become non-obvious? I
agree this is an important sort of a question to ask about use of theorem
proving for educational purposes. It is a cognitive psychology question and
cannot be expected to have a black and white answer, unlike a question such
as "is there a decision procedure". But I think that surely greater depth
of chaining can lead to steps that are less than obvious.
In section 2 of John Harrison's paper he uses an example of a theorem
"proposed by Los, as an example of a purely logical assertion which is
nevertheless not obvious. It is now often referred to by some name such as
nonobv (sic!) in the theorem proving literature; it is problem MSC006-1 in
the TPTP problem library". The theorem (cut and pasted from a different
source) is:
(!(x:'a) (y:'a) z. P x y /\ P y z ==> P x z) /\
(!x (y:'a) z. Q x y /\ Q y z ==> Q x z) /\
(!x y. P x y ==> P y x) /\
(!x y. P x y \/ Q x y)
==> (!x y. P x y) \/ (!x y. Q x y)
John proceeds to show a MESON proof of it. So there is a data point of a
theorem provable by MESON, for which there is some consensus that the
"step" of proving it is not obvious.
Also as Beeson points out in his MathXpert retrospective, as students
progress in studying mathematics, the appropriate step size changes
(increases) substantially as their skills improve. What is obvious to a
trained mathematician is likely to be non-obvious to a non-mathematician,
and so on.
I hope this helps.
-Cris
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
