Assumptions discharge, proof summary and labelling with bussproof

Question

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

Answer 1

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.)

Answer 2

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).

Answer 3

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!

Answer 4

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}