2

enter image description here

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 4

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

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}

enter image description here

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

1

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: enter image description here

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!

3
  • 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, 2015 at 6:57
  • Thank you! For (3) I found a really simple and intuitive solution...i posted it in this page.
    – Matteo
    Nov 16, 2015 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. Apr 21, 2016 at 19:18
0

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}

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .