2

With ebproof.sty package, one can write inference rules as

\begin{prooftree}
\hypo{A}
\hypo{B}
\hypo{C}
\infer3{D}
\end{prooftree}

to obtain the following:

A        B        C
___________________
         D

In my document, my A, B, and C hypotheses are quite long, so I would like to stack them above the inference rule, like this

    A
    B
    C
_________
    D

Is it possible to achieve such a typesetting with ebproof?

3 Answers 3

1

Use a matrix

\documentclass{article}
\usepackage{amsmath,ebproof}

\begin{document}

\begin{prooftree}
\hypo{\begin{matrix}
  AAAAAAAAAAAAAAAAAAAAAAA \\
  BBBBBBBBBBBBBBBB \\
  CCCCCCCCCCCCCCCCCC
\end{matrix}}
\infer1{D}
\end{prooftree}

\end{document}

enter image description here

4
  • I have extended the ebproof package to include the following extension here: ebproofx

You can redefine \infer to accept a comma-separated list (possibly a singleton list) to stack the premises as necessary:

\documentclass{article}
\usepackage{ebproof}
\ExplSyntaxOn
\int_new:N \g__ebproof_sublevel_int
\box_new:N \g__ebproof_substack_box
\seq_new:N \g__ebproof_substack_seq

\cs_new:Nn \__ebproof_clear_substack:
  {
    \int_gset:Nn \g__ebproof_sublevel_int { 0 }
    \hbox_gset:Nn \g__ebproof_substack_box { }
    \seq_gclear:N \g__ebproof_substack_seq
  }

\cs_new:Nn \__ebproof_subpush:N
  {
    \int_gincr:N \g__ebproof_sublevel_int
    \hbox_gset:Nn \g__ebproof_substack_box
      { \hbox_unpack:N \g__ebproof_substack_box \box_use:c { \__ebproof_box:N #1 } }
    \seq_gput_left:Nv \g__ebproof_substack_seq
      { \__ebproof_marks:N #1 }
  }

\cs_new:Nn \__ebproof_subpop:N
  {
    \int_compare:nNnTF { \g__ebproof_sublevel_int } > { 0 }
      {
        \int_gdecr:N \g__ebproof_sublevel_int
        \hbox_gset:Nn \g__ebproof_substack_box {
          \hbox_unpack:N \g__ebproof_substack_box
          \box_gset_to_last:N \g_tmpa_box
        }
        \box_set_eq_drop:cN { \__ebproof_box:N #1 } \g_tmpa_box
        \seq_gpop_left:NN \g__ebproof_substack_seq \l_tmpa_tl
        \tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl
      }
      { \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} \__ebproof_clear:N #1 }
  }

\cs_new:Nn \__ebproof_append_subvertical:NN
  {
    \bool_if:NTF \l__ebproof_updown_bool
      { \__ebproof_append_above:NN #1 #2 }
      { \__ebproof_append_below:NN #1 #2 }
  }

\cs_new:Nn \__ebproof_join_subvertical:n
  {
    \group_begin:
    \__ebproof_subpop:N \l__ebproof_a_box
    \prg_replicate:nn { #1 - 1 }
      {
        \__ebproof_subpop:N \l__ebproof_b_box
        \__ebproof_enlarge_conclusion:NN \l__ebproof_b_box \l__ebproof_a_box

        \__ebproof_make_vertical:Nnnn \l__ebproof_c_box
          { \__ebproof_mark:Nn \l__ebproof_b_box {axis} - \__ebproof_mark:Nn \l__ebproof_b_box {left} }
          { \__ebproof_mark:Nn \l__ebproof_b_box {right} - \__ebproof_mark:Nn \l__ebproof_b_box {left} }
          { \skip_vertical:N \l__ebproof_rule_margin_dim }
        \__ebproof_vcenter:N \l__ebproof_b_box
        \__ebproof_append_subvertical:NN \l__ebproof_a_box \l__ebproof_c_box

        \__ebproof_append_subvertical:NN \l__ebproof_a_box \l__ebproof_b_box
      }
    \__ebproof_push:N \l__ebproof_a_box
    \group_end:
  }

\cs_new:Nn \__ebproof_renew_statement:nnn
  {
    \exp_args:Nc \RenewDocumentCommand { ebproof#1 }{ #2 } { #3 }
    \seq_gput_right:Nn \g__ebproof_statements_seq { #1 }
  }

\cs_generate_variant:Nn \clist_map_inline:nn { xn }
\__ebproof_renew_statement:nnn { infer } { O{} m O{} m }
  {
    \group_begin:
    \__ebproof_restore_statements:
    \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
    \keys_set:nV { ebproof } \l_tmpa_tl
    \tl_set:Nn \l__ebproof_right_label_tl { #3 }

    \__ebproof_clear_substack:
    \clist_map_inline:xn { \clist_reverse:n { #2 } }
      {
        \__ebproof_join_horizontal:n { ##1 }
        \__ebproof_pop:N \l__ebproof_a_box
        \__ebproof_subpush:N \l__ebproof_a_box
      }
    \__ebproof_join_subvertical:n { \clist_count:n { #2 } }

    \__ebproof_push_statement:n { #4 }
    \__ebproof_join_vertical:
    \group_end:
  }
\ExplSyntaxOff

\begin{document}
\begin{prooftree*}
  \hypo{\Gamma \vdash 1}
  \hypo{\Gamma \vdash 2}
  \hypo{\Gamma \vdash 3}
  \hypo{\Gamma \vdash 4}
  \infer{3,1}{a}
  \hypo{\Gamma \vdash 5}
  \hypo{\Gamma \vdash 6}
  \hypo{\Gamma \vdash 7}
  \hypo{\Gamma \vdash 8}
  \hypo{\Gamma \vdash 9}
  \infer{2,1,2}{b}
  \hypo{\Gamma \vdash 10}
  \infer3{c}
\end{prooftree*}
\end{document}

stacked proof tree

ebproof uses a global stack to push and pop premises and conclusions. The above code defines another stack to hold premise-chunks to stack them vertically. Its structure is almost identical to what ebproof already does, and is compatible with existing codes AFAIK.

Caveat: It uses private implementation details, so it may break in the future.

1

One possibility is to use a tabular:

\documentclass{article}
\usepackage{ebproof}
\begin{document}
\begin{prooftree}
\hypo{\begin{tabular}{c}A\\B\\C\end{tabular}}
\infer1{D}
\end{prooftree}
\end{document}

enter image description here

You must log in to answer this question.