On Fri, Jul 20, 2012 at 12:21 AM, Bill Richter <
[email protected]> wrote:
> 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".
>
> Sorry, Freek, you're right. As I posted, I habitually use the term miz3
> to only mean the Mizar part of miz3, which is to say, not using tactics in
> the justifications. It's my goal to learn how to use tactics in miz3, to
> be writing proofs that are both declarative and procedural. It seems to me
> that everyone should formalize that way. How do you want folks to refer to
> the Mizar part of miz3, with no tactics in the justifications? This part
> is, I claim, much less powerful than HOL Light is generally, and you seem
> to agree:
>
> without explicit tactics I think you can prove _any_ theorem of the
> HOL Light logic with a sufficiently detailed miz3 proof.
>
> Yes, and you might need a ton of extra details, as Michael wrote:
>
> Though it might be tedious (perhaps extremely so) to do some
> things, I don't think there's anything preventing Tom Hales from
> doing all of the Kepler conjecture in structured miz3 proofs.
>
> Right, and that's what I mean by power. Hales estimated that formalizing
> his Kepler conjecture proof would take 20 man years, but that's using the
> full power of HOL Light. If Hales restricted himself to the Mizar part of
> miz3, with no tactics in the justifications, what's a good estimate? 40
> man years? 100 man years?
>
> Michael, that's clearly not your meaning of power:
>
> In this sense, miz3 *isn't* any more powerful than "straight
> FOL". (Given which, what in your experience makes you say that it
> is?)
>
> Yes, I'm in complete agreement, miz3 is only checking proofs FOL of mine,
> although as a technical point, with my Hilbert proofs I'm also making some
> use of the ZFC axioms encoded in HOL as well as Hilbert's f.o. geometry
> axioms.
>
> "by" is ultimately calling meson, a first-order proof procedure.
> Ignoring possible additional simplification that might happen
> first, meson is then looking for a first-order proof of your goal,
> using implication chaining and instantiation, and doing so to an
> arbitrary depth.
>
> Thanks, Michael, and I'm thinking about your heuristics from yesterday.
> But we should be able to put an upper bound on what miz3 can accomplish
> with MESON and simplifications (can you expand on simplification BTW?) if
> it justifies a statement alpha with the miz3 line
>
> alpha by X1, X2, ....;
>
> Like all other first order systems (e.g., Vampire), all you can say
> is that it will prove some goals and won't prove others
>
> According to Josef Urban, Vampire is clearly more powerful than the Mizar
> part of miz3, as it proved with no instructions all but 4 of my theorems in
> 1000 lines of Tarski geometry code.
>
> Indeed, if you were using Isabelle, you could link the equivalent
> of "by" directly to Vampire or some other modern first order prover
> and probably find that you could make rather larger jumps than
> previously.
>
> That's interesting! But that's my whole point: I don't want the Mizar
> part of miz3 to be able to make overly large jumps. I know from
> experience that there's a lot of hit & miss on exactly how large a jump I
> can get away with. Sometimes I can combine 3 lines of code into 1, and
> sometimes I think miz3 will prove something and I time out, so I put in
> another line or two of the proof. I don't need to have this explained
> precisely. I'm sure that's in your heuristics. But I want to be able to
> explain in my Geometry paper that there's a reasonable upper bound on what
> miz3 can do. Back to your
>
> "by" is ultimately calling meson, a first-order proof procedure.
> Ignoring possible additional simplification that might happen
> first, meson is then looking for a first-order proof of your goal,
> using implication chaining and instantiation, and doing so to an
> arbitrary depth. In this sense, miz3 *isn't* any more powerful
> than "straight FOL".
>
> Ok, let's allow miz3 to do all possible simplifications with no bound on
> the depth and no time-out. That would be unusable, because miz3 would
> never catch any of my numerous obvious blunders. But we should be able to
> describe what the miz3 by (sans tactics) could prove that way.
>
Bill, are you aware of John Harrison's paper "Optimizing Proof Search in
Model Elimination"
(http://www.cl.cam.ac.uk/~jrh13/papers/me.html)? He tested various
heuristics for bounding the Meson search including I think the one actually
used by MESON_TAC today. From the point of view of education and
predictability of what the prover will and won't do, a simple limit on
depth of chaining has sounded interesting to me, and that is one of the
options he tested.
-Cris
>
> --
> 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
>
------------------------------------------------------------------------------
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
