Heuristics for optimal traversal for LowerUnivalents

[ceilican]

I have read the explanation of the example of compression with LUniv, and I noticed that it depends on a particular top-down traversal order, in which the unit {a} is visited before the subproof of {-a,b}. Otherwise, no compression would have happened.

I know that, in general, LUniv will always be dependent on the traversal order, because whether a subproof is univalent depends on the subproofs that have already been collected.

It could make sense to investigate heuristics that try to traverse the proof in the best possible top-down order... In the case of LUniv, it might be beneficial to visit subproofs with smaller conclusions first, for example... Probably the gain would not be so significant, though.

[ceilican]

Joseph's comment:

I thought about the ordering for LUniv long time ago. I just remembered it
writing the example. I tought about two directions. First, we could try to
tweek the order Proof are linearized. Unfortunately I postponed this
investigation until I forgot about it. The second direction was to search for
an heuristic. But this would require a preprocessing traversal which would
have make it impossible to use LUniv to combine LU after RPI. This combination
was my main goal and that's why I discarded this direction.

[ceilican]

Duplicate of issue #58 .