On 21 Jul 2012, at 05:49, Bill Richter wrote: > Chris, your MESON example was illuminating, and I hope someone can tell me > what it means. Paste this code from p 36 of John's tutorial into the HOL > Light window: > > MESON[] > `(!x y z. P x y /\ P y z ==> P x z) /\ > (!x y 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)`;; > > MESON solves this logic puzzle (which I still haven't yet solved) quite > quickly, and it writes > ...solved at 23107
Your post inspired me to write up an "intuitive" proof of Los's non-obvious theorem, see https://dl.dropbox.com/u/34693999/nonobv.pdf. As I say in the write-up, whether an "intuitive" proof is better or worse than what an ATP produces is a matter of opinion. In fact, a fairly mindless approach by a human being will come up with a low-level proof of the non-obvious theorem without too much effort. It took me a lot longer to come up with something that actually feels like it is using the apparent structure in the problem. Specifically, the fact that P is very nearly an equivalence relation seems to a human quite important, but you have to work to get a conceptual proof that exploits that. Human beings deliberately try to find proofs that use familiar concepts. Machines don't need the warm feelings that that gives. It seems to me that it is a really deep AI challenge to try to produce mechanized theorem proving systems that are usable and don't suffer the Frankenstein effect (whereby the monster you create displays emergent behaviour that goes fair beyond your own abilities). This is, I think, what you and Mark Adams and others want for pedagogical purpose and I think it is actually a much, much harder challenge than working towards mechanized theorem proving systems that are "merely" powerful and usable (and include decision procedures and heuristics that go way beyond human capabilities). In some sense, this issue already arises in mathematics without mechanization: in the foreword to Freek Wiedijk's Seventeen Provers of the World, Dana Scott writes: `As I have often told students, “Algebra is smarter than you are!” By which I mean that the laws of algebra allow us to make many steps which combine information and hide tracks after simplifications, especially by cancellation. Results can be surprising, as we know from, say, the technique of generating functions.' Ordinary mathematical practice already involves powerful conceptual tools that have surprising consequences. So I am impressed by endeavours to implement mechanized systems for mathematics that mimic human capability without giving any surprises, but I prefer easier challenges myself! Regards, Rob. ------------------------------------------------------------------------------ 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
