Even if we fix the proof tool as "miz3 with MESON only (no other tactics)",
there is still potential confusion about what "power" might mean. Here are
some possibilities. You should probably pick one before discussing further:
1. Which theorems is it theoretically possible to prove? (I think we all
agree that the answer is "all the theorems of HOL".)
2. Which theorems is it theoretically possible to prove with a resource
bound (e.g. lines of proof script, or time/memory to run the proof script).
This is a family of questions, and I'm not sure anyone will have any good
data on the answers...
3. Which theorems is it possible for Bill Richter to prove (optionally
with an additional resource bound)? (No idea...)
On Fri, Jul 20, 2012 at 8: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.
>
> --
> 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
