Thanks, John!  I'll fiddle with the miz3 term `set' and book up in the
Mizar literature.  This is excellent:

   Yes, this may be the core problem: the default built-in miz3 prover
   doesn't know much about sets, and may not know that, say, the
   formulas S = {x | P x} and !x. x IN S <=> P x are equivalent, as
   you might have expected. There is a standard HOL Light tactic
   called SET_TAC that does some preprocessing of set operations and
   then calls MESON. It would certainly be possible to change the
   default miz3 prover to do something similar.

Thanks!  That really helps my faith in HOL Light.  That would be great
if you or Freek could make this improvement.

   You are probably going to hit quite a few such restrictions as you
   are using miz3 pretty heavily, and it may make sense for us to
   improve the default miz3 prover as you hit these issues rather than
   have you work around them. However, I am a bit short of time to
   work on it right now so I can't promise to fix these shortcomings
   myself in the short term.

Can we make a deal?  If I code up the Hilbert plane geometry part of
my paper (18+ pages), can you fix it by the time I'm done?  I think it
would be easy to modify my worked-around code if you fix it by then.

-- 
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to