Hi Bill, >I think miz3 is much less powerful than HOL Light is generally.
Sorry to disagree, but this seems wrong to me. This is only true if you don't put tactics in the justifications. I especially allow _arbitrary_ HOL Light tactics there for exactly this reason: so miz3 would be just as "powerful" as "HOL Light generally". In fact, the miz3_of_hol code can automatically convert arbitrary HOL Light tactic scripts to miz3 proofs. (Actually the parser in the current code can only handle John's tactic script conventions, but the _approach_ can handle _any_ HOL Light tactic script.) And even without explicit tactics I think you can prove _any_ theorem of the HOL Light logic with a sufficiently detailed miz3 proof. The ten inference rules of the HOL Light logic certainly seem within the power of miz3's "by", bad as it is :-) Freek ------------------------------------------------------------------------------ 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
