# Assumptions discharge, proof summary and labelling with bussproof

Is it possible with bussproof package obtain this kind of formula-layout?:

(1) Assumptions discharge with four vertical dots;

(2) Four vertical dots for proof summary;

(3) Labelling with a number (in this case "1.") over a formula.

Thank you

## 4 Answers

Trying using the \noLine option. For instance, to get a "1." above "[A]" above dots, use:

\AxiomC{\small 1.}
\noLine
\UnaryInfC{[$A$]}
\noLine
\UnaryInfC{$\vdots$}


The \vdots gives only three dots. One way to get four dots is define a LaTeX command to place four periods vertically in a vbox. Alternately, the LaTeX "stix dots" package includes a \fourvdots command.

\small should give small font (alternate: \footnotesize)

The \extraVskip command can be used to adjust the white space between lines in the derivation.

(Caveat: I have not tested to code above in an actual LaTeX file. If there are any bugs in the code, let me know and I can update.)

I tried with this code

\begin{center}
\AxiomC{$A \vee B$}
\alwaysNoLine
\AxiomC{[$A$]}
\UnaryInfC{\vdots}
\UnaryInfC{$C$}
\AxiomC{[$B$]}
\UnaryInfC{\vdots}
\UnaryInfC{$C$}
\alwaysSingleLine
\TrinaryInfC{$C$}
\DisplayProof
\hspace{25pt}
\alwaysNoLine
\AxiomC{\small 1.}
\UnaryInfC{[$A$]}
\alwaysSingleLine
\UnaryInfC{$A \to B$}
\DisplayProof
\end{center}


I used \alwaysNoLine instead of \noline. That is the result for (1) and (3) instances:

Unfortunately, there's too much space between formulas in square brackets. There's a new package called prftree.sty where is possible obtain those kind of layout but 1) it's not intuitive as bussproof; 2) I can't use it because it goes in contrast with bussproof and I don't have time to change every formula wrote earlier with bussproof.

Anyway thank you for your help!

• I presume you mean there is too much space separating the formulas in square brackets from the \vdots. You can adjust this in two ways: First option, if you do not need to doit very often, adjust the \extraVspace to be less than the default 2pt, perhaps even to a negative value. Second option that works better if you are using it a lot: define a different version of \vdots that is in a box with less height. – Sam Buss Nov 15 '15 at 6:57
• Thank you! For (3) I found a really simple and intuitive solution...i posted it in this page. – Matteo Nov 16 '15 at 14:03
• @SamBuss I'm assuming you've at some point determined a good size box to put \vdots in for this purpose. I'm curious what you've found and if you might want to share your code. – Shay Apr 21 '16 at 19:18

The ebproof package provide an handy solution:

\documentclass{article}
\usepackage{ebproof}
\usepackage{xcolor}
\begin{document}
\begin{tabular}{ c c c }
{\color{red}\textbf{(1)}}
\begin{prooftree}
\Hypo{A \vee B}
\Hypo{[A]}
\Ellipsis{}{C }
\Hypo{[B] }
\Ellipsis{}{C }
\Infer3[$\vee\textrm{E}$]{C}
\end{prooftree}
&
{\color{red}\textbf{(2)}}
\begin{prooftree}
\Hypo{}
\Ellipsis{}{ A}
\Hypo{}
\Ellipsis{}{ B}
\Infer[no rule, separation=-0.4em, rule margin=-.3em]2{}
\Ellipsis{}{C}
\end{prooftree}
&
{\color{red}\textbf{(3)}}
\begin{prooftree}
\Hypo{\stackrel{1}{[A]}}
\Infer[right label ={$$\supset I.1.$$}]{1}{A \supset A}
\end{prooftree}
\end{tabular}
\end{document}


Especially considering the fact that space can be easily adjusted (have a look at the documentation, section 4.2, Spacing).

For schema n. (3) I found a really simple solution. Using bussproof, the code is:

\begin{prooftree} \AxiomC{[$\overset{1.}{A}$]} \UnaryInfC{$A \to B$} \end{prooftree}

• \stackrel{1}{[A]}, that I proposed in my solution, is probably a nicer way to obtain this result. – Clément Nov 16 '15 at 16:08