I have another newbie question regarding HOL Light; again happy to hear about other HOL variants if those have easier answers.
I'm in the typical post-human-proof situation where a program found a "proof" that's too tedious for a human to verify (in the conventional sense, not PCPs). For verification, I'm converting the "proof" into a HOL Light proof: auto-generating the whole chain of intermediate steps as definitions, and auto-generating all the theorems linking the definitions. This works fine on scaled-down examples, and extrapolation suggests that the CPU time for HOL Light will still be affordable when scaled up to the full theorem, in the ballpark of 10000 core-hours. It's no problem to farm the separate proof steps out to separate cores, each using its own subset of the relevant definitions, at which point I have one instance of HOL Light printing out a theorem saying A implies B, and a separate instance of HOL Light printing out a theorem saying B implies C, and so on. This brings me to the question: how can I have HOL Light printing out the combined theorem saying that A implies Z, without waiting 10000 hours for HOL Light on one core to serially run through proving all the lemmas? I'd guess that >99% of the CPU time I'm seeing comes from HOL Light searching for proofs (e.g., the computation in REAL_LINEAR_PROVER), and that far less is spent by the HOL Light kernel verifying the proofs. Is there a generic mechanism to record merely what the kernel is doing--- i.e., to automatically write down a proof in the conventional sense--- and then replay this proof in another HOL Light instance that has the same definitions? The papers I've found on the problem of exporting libraries of theorems from one system to another sound like that's only partially solved, but that's also a conceptually more difficult problem than simply replaying the lowest level of proof within a single system. I did various other searches for answers and didn't find anything---sorry if I missed something obvious. In general the small kernel makes me think that tracing proofs wouldn't be touching many lines of code, but I haven't studied the kernel closely enough to be confident about this. In case this (1) doesn't exist and (2) is hard to build, my backup plan is to modify the program printing out the proof tactics to do its own searches for lower-level proof steps. Conceptually this would be copying the searches implemented in HOL Light, so presumably the speed will end up similar, but the searches would then be easily distributable precomputation, which is the objective---I'd just like to reach this without the waste of time of reimplementing something that HOL Light already knows how to do! ---Dan
signature.asc
Description: PGP signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
