Combination of LU and LUniv (and LUniv's traversal order dependence)

[ceilican]

To Joseph:

I have read the paper's 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. But in the particular case of units, it seems that we could avoid this order dependence if we first selected all the units in an extra traversal. Have you considered this?

Another thing: do you think it would 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, right? What do you think?

[ceilican]

From Joseph:

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.

But now, this second direction is really interessing, indeed. I would like to have some time to investigate it. Maybe this summer.

But in the particular case of units, it seems that we could avoid this order dependence if we first selected all the units in an extra traversal. Have you considered this?

This one is easy to implement and should have been. It's only about combining LUniv after LU.

[ceilican]

From Joseph:

About our previous idea to implement LUniv after LU, did you mind the difficulty arising with subproof of the lowered units ?

[ceilican]

Which difficulty?

[Jogo27]

The difficulty to know where to reintroduce univalent subproofs w.r.t. units.

The most obvious order is to reintroduce univalents above units, such that units' duals may be added to Delta. But let's suppose a subproof phi_s of a unit phi_u is univalent with valent literal ell. First phi_s is deleted, which cause dual{ell} to be added to phi_u's conclusion. Then phi_s is reintroduce, but above phi_u. Therefore dual{ell} from phi_u is not deleted and is added to proof 's conclusion.

A first solution might be just to not lower univalents in units. But even this simple (and probably inefficient) solution is not such easy to implement because LUniv is a top-down traversal. Keeping track of whether a given subproof is a subproof of a unit involves having a dict of bool and therefore would need unnegligeable quantity of memory.

A more complicated solution is not only to keep track of to which unit any node belongs to, but to insert carefully each lowered subproof in a list corresponding to the reintroduction order. I allready tried this kind of implementation which allows the traversal to be bottom-up. The drawback is that it'll probably be a quadratic time complexity algorithm.

[ceilican]

I see. It seems it is not as trivial as I first thought. Let's keep this issue as low priority and focus our attention on issue #57 instead, which seems more elegant and more promising.

[ceilican]

Moreover, if we decide to investigate this issue further in the future, perhaps we should first make some experiments with sequential composition of LUniv and LU. This might give us an idea whether a complicated non-sequential combination of LU and LUniv is worth.

[Jogo27]

Sorry but I don't think a sequential composition of LUniv after LU could give us an idea whether combining LU and LUniv could be worth. Because the advantage of the combination is to already have all the duals of units in Delta while starting to check for univalent subproofs. For a sequential composition we won't have any garantee units would be considered for lowering first.