The SVG visualization of proof trees, as originally written by @bbonf in #51 and as operationalized in #79, makes the simplifying assumption that sibling subtrees have equal width. The width of a parent tree is determined as twice the maximum of the width of its subtrees. This has the advantage that the parent can always be centered between its subtrees, which means the root is always at the middle of the top edge of the visualization. The subtrees are also positioned such that the connecting brace can be symmetrical.
While this simplification is helpful, it results in a lot of wasted horizontal space. A good example of this is the entailment proof of the first SICK problem. Users have to scroll large distances horizontally, passing large stretches of emptiness. The stronger the branching of the proof tree, the stronger this effect becomes as wasted space multiplies and accumulates.
I think a better approach would be to not take twice the maximum subtree width, but simply the sum of the subtree widths in order to determine the parent width. The nodes of the parent tree could be centered at half this combined width, in order to preserve the horizontal centering of the root node. The one sacrifice we would have to make, is that the braces connecting a parent to its subtrees would get unequal lengths.
The SVG visualization of proof trees, as originally written by @bbonf in #51 and as operationalized in #79, makes the simplifying assumption that sibling subtrees have equal width. The width of a parent tree is determined as twice the maximum of the width of its subtrees. This has the advantage that the parent can always be centered between its subtrees, which means the root is always at the middle of the top edge of the visualization. The subtrees are also positioned such that the connecting brace can be symmetrical.
While this simplification is helpful, it results in a lot of wasted horizontal space. A good example of this is the entailment proof of the first SICK problem. Users have to scroll large distances horizontally, passing large stretches of emptiness. The stronger the branching of the proof tree, the stronger this effect becomes as wasted space multiplies and accumulates.
I think a better approach would be to not take twice the maximum subtree width, but simply the sum of the subtree widths in order to determine the parent width. The nodes of the parent tree could be centered at half this combined width, in order to preserve the horizontal centering of the root node. The one sacrifice we would have to make, is that the braces connecting a parent to its subtrees would get unequal lengths.