Hi Michael, Okay, final mail I'm sending about this:
>1. miz3's "by" is designed (i.e., someone intentionally >chose to do this) with a time limit. Well, the time limit even is there if you put a tactic there yourself. So I would distinguish between the default "by" prover, and the time limit thing. But apart from that: yes. >2. The time limit means that miz3's "by" proves fewer >goals than it might without the time limit. Yes. Although in practice it won't be so different. A justification failing because of the time limit is rare. Generally it means that it just doesn't hold. >3. A system A that proves fewer things than system B is a >"weaker" system than B. Yes! >4. So, miz3 is intentionally weakened. There's no flaw in your logic :-) I fully agree. 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
