How do I display a proof tree with HTML,CSS and/or Javascript?

Question

I want to display a proof tree in the style of a natural deduction within a web page. I will get the data from a JSON file.

Whats the best way to display something like this? Is it possible only with css? Or is there a library that can do something like this? Rendering as an image is not possible, because eventually it should be interactive. I should also mention that this tree can get fairly large.

Example:

Update: A better example of what the end result should look like:

Answer 1

So after much fiddling with css, I used tables to get a satisfactory result. Since the layout is indeed part of the semantics, I think its acceptable in this case.

A small example would look like this:

<table>
    <tr>
        <td>
        </td>
        <td class="rulename" rowspan="2"><div class="rulename">add</div></td></tr>
    <tr><td class="conc">conclusion</td></tr>
</table>

And the css:

td {
 text-align:center;
 height: 1em;
 vertical-align:bottom;
}
td.conc {
 border-top: solid 1px;
}
div.rulename {
 margin-top:-2em;
}

Bigger demo

Answer 2

The easiest solution would be mathjax which is a latex javascript renderer. And there are quite a few other similar rendering options out there.

Alternatively you could also look at MathML, which is the w3c standard for writing mathematical equations. Sadly, right now, the support for it is quite lacking as can be seen here, but long term it's going to be a great solution. Additionally the previously mentioned MathJax can be used as a MathML shim in browsers that do not support MathML yet.

The only concern with the MathJax shim is going to be that when you make it interactive it's going to interact differently with your code in browsers which do and do not support MathML, but despite that I would personally advice MathML except if you're already bound into LaTeX.

Based on your update I am not sure whether that can be expressed in MathML or LaTeX and I fear the only thing you could do is draw it on a canvas or set it up in a SVG if you need the interactivity later on. But I can warn you already know that that's not going to be a simple thing to do if you aren't used to it.

---

To add interactivity to Mathjax:

1. Use MathML as input
2. Use HTML/CSS as output
3. Disable the MathJax context menu by adding showMathMenu:false to your core MathJax config
4. Include id's in your MathML markup (literally <mo id="someid"> for example)
5. Use for example jQuery to bind to the id after MathJax has finished (i.e. $("#someid").on("mousemove",function(){...}))

A fully working demo can be found here, move over the equal sign to trigger an alert.

Answer 3

I came across the same thing recently, and I managed to write some CSS which gives quite good results I think. Here's a sample html skeleton:

<div class="proof">
    <div class="prems">
        <div class="proof">
            <div class="prems">
                <div class="proof">
                    <div class="prems">
                        <div class="proof">
                            <div class="concl">
                                <div class="concl-left"></div>
                                <div class="concl-center">bla</div>
                                <div class="concl-right"></div>
                            </div>
                        </div>
                        <div class="inter-proof"></div>
                        <div class="proof">
                            <div class="concl">
                                <div class="concl-left"></div>
                                <div class="concl-center">bla</div>
                                <div class="concl-right"></div>
                            </div>
                        </div>
                    </div>
                    <div class="concl">
                        <div class="concl-left"></div>
                        <div class="concl-center">bla</div>
                        <div class="concl-right"></div>
                    </div>
                </div>
                        <div class="inter-proof"></div>
                <div class="proof">
                    <div class="concl">
                        <div class="concl-left"></div>
                        <div class="concl-center">bla</div>
                        <div class="concl-right"></div>
                    </div>
                </div>
            </div>
            <div class="concl">
                <div class="concl-left"></div>
                <div class="concl-center">bla</div>
                <div class="concl-right"></div>
            </div>
        </div>
    </div>
    <div class="concl">
        <div class="concl-left"></div>
        <div class="concl-center">blabla</div>
        <div class="concl-right"></div>
    </div>
</div>

and here's the CSS:

.proof
{
    display: inline-flex;
    flex-direction: column;
}
.prems
{
    display: inline-flex;
    flex-wrap: nowrap;
    align-items: flex-end;
}
.inter-proof
{
    border-bottom: 1px solid black;
    width: 1em;
}
.concl
{
    display: inline-flex;
    margin-top: -1px;
}
.concl-left
{
    flex-grow: 1;
}
.concl-center
{
    border-top: 1px solid black;
}
.concl-right
{
    flex-grow: 1;
}
.prems > .proof:not(:first-child) > .concl > .concl-left
{
    border-bottom: 1px solid black;
}
.prems > .proof > .concl > .concl-center
{
    border-bottom: 1px solid black;
}
.prems > .proof:not(:last-child) > .concl > .concl-right
{
    border-bottom: 1px solid black;
}

see it live here. I only tried with firefox, and it may need some tweaks for other browsers.

Answer 4

I gave it a try (for this) and here are the codes (using just plain css and javascript). It just draws raw strings like this image (so no LaTeX... but I also want to accomplish this and currently trying ).

The starting point was something like below.

<style>
  #proof-tree {
      padding: 50px;
      overflow-x: scroll;
  }
  .node {
      display: inline-block;
      white-space: nowrap;
      margin: 0 2em;
      text-align: center;
  }
  .bar {
      width: 100%;
      height: 1px;
      background: black;
      position: relative;
  }
  .rule {
      position: absolute;
      bottom: -0.5em;
      right: -3em;
  }
</style>

<div id="proof-tree">
  <div class="node">
    <div class="antecedents">
      <div class="node">
    <div class="antecedents">
      <div class="node">
        <div class="antecedents"></div>
        <div class="bar"><div class="rule">rule1</div></div>
        <div class="consequent">foo1</div>
      </div>
      <div class="node">
        <div class="antecedents"></div>
        <div class="bar"><div class="rule">rule2</div></div>
        <div class="consequent">hoo2</div>
      </div>
    </div>
    <div class="bar"><div class="rule">rule3</div></div>
    <div class="consequent">foo3</div>
      </div>
      <div class="node">
    <div class="antecedents"></div>
    <div class="bar"><div class="rule">rule4</div></div>
    <div class="consequent">foo5</div>
      </div>
    </div>
    <div class="bar"><div class="rule">rule6</div></div>
    <div class="consequent">foo6</div>
  </div>
</div>

It displays like this.

However, in this way, the lower bars tend to be too long and I couldn't get satisfied with it. Therefore, I wrote some javascript to get the position of nodes and minimize the length of the bar. I do NOT think this is the smartest idea at all. It is obviously dirty... but I hope this could be any help to someone (like me).

Also, please let me know if you/someone have any additional info.