Re:Two-hundred-terabyte math proof is largest ever
by CJefferson on Friday May 27, 2016 @07:55AM
(#11785376)
I've had a similar problem, there is nothing that useful I'm afraid. Probably best to look into general discussions of trees.
One thing worth trying to do (if you can) is separate the generation of the tree from the tree itself -- hopefully you can imagine the tree existing as a complete object (even though you never store it all), and formulate proofs based on that.
Re:Two-hundred-terabyte math proof is largest ever
by clarus on Friday May 27, 2016 @12:59PM
(#11787302)
In the community of the theorem prover Coq, a proof obtained by running a proven correct decision procedure is called a "proof by reflection".
There is also the "proof by certificate" approach. You generate a potentially large proof certificate by an unverified program. Then you run a proven correct (small) checker on the certificate to concude that the theorem is correct.
When you encode the search tree as a proof, is there a technical name for that technique?
In my situation I encoded the proof as a sequence which is just the depth-first linear labelling of the tree. Then I proved why the sequence represents a proof. But if there is a most standard terminology/literature on this step, it would make it easier for me to talk about.