# Tableau proof with boxes

How do I draw a tableau proof like the one in the following picture?

I would like to have the boxes with their table-like structure:

• The numbers on the left side
• The formulas in the center
• The other numbers on the right side
• The optional horizontal line
• The colored tet on the bottom

The connections between those boxes are also important for me.

Colors and the borderstyle are not that important but would be a nice-to-have feature.

Is there a package for this or can this somehow be done using tikz?

• Welcome to TeX.SX! On this site, a question should typically revolve around an abstract issue (e.g. "How do I get a double horizontal line in a table?") rather than a concrete application (e.g. "How do I make this table?"). Questions that look like "Please do this complicated thing for me" tend to get closed because they are either "off topic", "too broad", or "unclear". Please try to make your question clear and simple by giving a minimal working example (MWE): you'll stand a greater chance of getting help. – Stefan Pinnow Jun 2 '19 at 18:57
• Thank you for this advise. Since my question is solved, should I update my question to be more abstract or should I leave it as it is? – p0kR Jun 2 '19 at 22:19
• Then you were lucky that someone did all the work himself and you can let your question as is. Luckily for us -- the other users -- is, that the answer is an MWE ... – Stefan Pinnow Jun 3 '19 at 4:25

Welcome to TeX-SE! This is to give you a start. I did not have the passion to punch in the formulae completely but from what is there you will be able to complete them. The diagram is a tree, for which I recommend forest. The tables can be obtained with simple arrays. (The coloring can be done automatically if there are clear rules how the color depends on the location.)

\documentclass{article}
\usepackage[edges]{forest}
\usetikzlibrary{backgrounds}
\usepackage{amsmath}
\usepackage{marvosym}
\begin{document}
\begin{forest}
for tree={l sep+=0.5em,parent anchor=south,child
anchor=north,fill=yellow!40,draw,dotted},
forked edges
[$\begin{array}{lcc} {}^*0 &\lnot ( p\lor (q\land r))\to (p\lor q)\land (p\lor r) & 1\\ \phantom{{}^*}1\text{a} &\dots& 2\\ \phantom{{}^*}1\text{b} &\dots& 4\\ \end{array}$
[$\begin{array}{lcc} 2\text{a} &p& ~\\ \end{array}$
[$\begin{array}{lcc} 0 &\dots & 1\\ 1\text{a} &\dots& 2\\ 1\text{b} &\dots& 4\\ \hline \multicolumn{3}{c}{\textcolor{red}{\text{\Lightning,2a,5a}}} \end{array}$,fill=yellow!70
]
[$\begin{array}{lcc} 0 &\dots & 1\\ 1\text{a} &\dots& 2\\ 1\text{b} &\dots& 4\\ \hline \multicolumn{3}{c}{\textcolor{red}{\text{\Lightning,2a,5a}}} \end{array}$,fill=yellow
]
]
[$\begin{array}{lcc} 2\text{b} & q\land r & 3\\ 3\text{a} & q & \\ 3\text{b} & r & \\ \end{array}$
[$\begin{array}{lcc} 0 &\dots & 1\\ 1\text{a} &\dots& 2\\ 1\text{b} &\dots& 4\\ \hline \multicolumn{3}{c}{\textcolor{red}{\text{\Lightning,2a,5a}}} \end{array}$,fill=yellow!70
]
[$\begin{array}{lcc} 0 &\dots & 1\\ 1\text{a} &\dots& 2\\ 1\text{b} &\dots& 4\\ \hline \multicolumn{3}{c}{\textcolor{red}{\text{\Lightning,2a,5a}}} \end{array}$,fill=yellow
]
]
]
\begin{scope}[on background layer]