如何使用 ebproof 堆积假设

Question

使用ebproof.sty包，可以编写推理规则如下

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

获得以下内容：

A        B        C
___________________
         D

在我的文档中，我的A、B和C假设很长，所以我想把它们堆叠在推理规则之上，就像这样

    A
    B
    C
_________
    D

可以用 实现这样的排版吗ebproof？

Answer 1

用一个matrix

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

\begin{document}

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

\end{document}

Answer 2

• 我已经扩展了 ebproof 包以包含以下扩展：ebproofx

---

您可以重新定义\infer以接受逗号分隔的列表（可能是单例列表）以根据需要堆叠前提：

\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}

ebproof使用全局堆栈来推送和弹出前提和结论。上面的代码定义了另一个堆栈来保存前提块，以垂直堆叠它们。其结构与ebproof现有的几乎相同，并且据我所知与现有代码兼容。

警告：它使用私有的实现细节，因此将来可能会出现故障。

Answer 3

一种可能性是使用表格：

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