Hi Bill,
| I would tend to think your focused approach to permutations isn't general
| enough, but I'm no expert. I did read some of your book, the Mizar-like
| section, and it seemed to me that you said something really important:
| neither of the following approaches is very good:
|
| 1) get the computer to go prove the theorem;
| 2) tell the the computer exactly how to go prove the theorem;
| and the winning strategy is to combine (1) & (2).
I agree absolutely that focusing on the special case of simple
permutation of arguments is unsatisfyingly specialized. I suspect,
however, that if you go too far beyond it then things may well become
undecidable. So even if one wants (1), it might not be feasible,
though it would be very interesting to investigate the boundary and
perhaps find interesting decidable subsets or useful heuristics.
HOL Light, in common with some other proof assistants, has a few
tricks for permutative rewrites so that things can be "normalized" by
rewriting with suitable theorems, e.g.
let trivial_example = prove
(`{a,c,d,d,a,b} = {d,a,b,c}`,
REWRITE_TAC[INSERT_AC]);;
This idea goes back at least to Boyer and Moore, and there is a nice
paper "Ordered Rewriting and Confluence" by Ursula Martin and Tobias
Nipkow that shows it off on many examples. However, as soon as you
combine even this kind of simple permutative reasoning, let alone
general set equivalence, with quantifier instantiation, matters are
substantially more complicated. Konrad Slind's paper "AC unification
in hol90" describes a HOL implementation of associative-commutative
unification, which is one approach to such problems.
John.
------------------------------------------------------------------------------
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
