On 24 June 2011 01:32, Michael Norrish <[email protected]> wrote: > 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.
For correct hypotheses, a few seconds, and longer for incorrect ones, but not massive amounts of time. Obviously this method is far from ideal, but because of the simplicity of the hypotheses, it was actually working acceptably (apart from the bug). > >> 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. Any ideas how to find these? I've attempted to run it with tracing enabled, but there's a massive amount of spewage and i'm not really sure what to look for. > In general, METIS_TAC is designed to be used with smallish numbers of > theorems. > > I hope this helps, > Michael > > Thanks for your help, Tom ------------------------------------------------------------------------------ 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
