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.