On 23/06/11 21:33, Tom N wrote: > I have a set of hypotheses involving the words library that I would > like to prove automatically. My first attempt at this was to ask HOL > to prove them against the entirety of wordsTheory, using:
> > prove(hypothesis, METIS_TAC(map snd (DB.theorems "words"))); Wow. How long do these attempts take? I'd be very surprised if you got many interesting results out of this. > While this appeared to work at first, it seems that it is able to > 'prove' obviously-incorrect hypotheses, for example: > > load "wordsTheory"; open wordsTheory; > > show_assums := true; > > prove(``F``, METIS_TAC(map snd (DB.theorems "words"))); > [%%genvar%%8939 = @m. dimindex (:'XXfolXX_40996) = SUC m, > %%genvar%%8939 = @m. dimindex (:2) = SUC m, > %%genvar%%8939 = @m. dimindex (:unit) = SUC m] |- F: > thm > Is this more likely to indicate an inconsistency in wordsTheory, or me > doing something wrong? I've only started using HOL recently, so it's > probably the latter ;) It's a bug in METIS_TAC, strictly. The theorem is OK (though not informative); the second and third assumptions are equivalent to the statements %%genvar%%8939 = 1 and %%genvar%%8939 = 0 which is how false can be derived. It's a bug because METIS_TAC should not be adding assumptions to the goal it's trying to prove. It would be interesting to know just which theorems in wordsTheory were giving rise to this derivation; they would help us track down the problem in METIS_TAC. In general, METIS_TAC is designed to be used with smallish numbers of theorems. I hope this helps, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense.. http://p.sf.net/sfu/splunk-d2d-c1
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
