Is there a way to draw bussproof style tree diagram in Jupyter Notebook?

Question

An example of bussproof style tree diagram is shown below.

Above diagram shows the AST(abstract syntax tree) of the propositional formula $\neg A \to (B \vee C)$. Such a diagram can be drawn using the LaTeX package bussproof.sty.

I am aware that I could use graphviz for drawing AST, but somehow I prefer the simple bussproof style diagram. So here is my question: is there a way to draw bussproof style tree diagram for logical formulas and/or Natural deduction proof in Jupyter Notebook?

I tried graphviz, treelib, and plotly. None of these were satisfactory. I want bussproof style diagram.

Answer 1

I have created a Python script that generates busproof-style tree diagrams. This script is compatible with Jupyter Notebook and can also be used on the Google Colab platform. You can access the script here.

The script also generates LaTeX source that can be used with bussproofs.sty.

It includes parser for propositional logic. So the following code generates (1) the LaTeX source and (2) the tree diagram.

input_formula = "not A imp B imp not C and D"
testParser(input_formula, 'bussproof')
testParser(input_formula, 'tree')

Generates the following LaTeX source

\begin{prooftree}
\AxiomC{$A$}
\UnaryInfC{$\neg$}
\AxiomC{$B$}
\AxiomC{$C$}
\UnaryInfC{$\neg$}
\AxiomC{$D$}
\BinaryInfC{$\wedge$}
\BinaryInfC{$\rightarrow$}
\BinaryInfC{$\rightarrow$}
\end{prooftree}

and the following diagram.