I have a question about computer-generated proofs, as I am doing something similar.
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.
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.
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.