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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
