Как написать правила вывода, если у нас есть два антецедента

Question

\[ \frac{A \rightarrow f[\overrightarrow{B}]:= \Psi \\ \Phi \in
\langle\Psi\rangle} {A \rightarrow f[\bullet\overrightarrow{B}];\Phi} \]

Мне нужно разместить два антецедента в двух отдельных строках.

A \rightarrow f[\overrightarrow{B}]:= \Psi

\Phi \in \langle\Psi\rangle

Answer 1

Хотя я не знаком с контекстом, вы можете использовать an arrayдля разбиения «антецедентов» на отдельные строки:

\documentclass{article}
\begin{document}
\[
  \frac{\begin{array}{@{}c@{}}
    A \rightarrow f[\overrightarrow{B}]:= \Psi \\
      \Phi \in \langle\Psi\rangle
  \end{array}}{
    A \rightarrow f[\bullet\overrightarrow{B}];\Phi}
\]
\end{document}

Это поместит объект вертикально по центру дробной линии. Если это не имеет значения, вы можете сделать все внутри окружения array:

\[
  \begin{array}{c}
    A \rightarrow f[\overrightarrow{B}]:= \Psi \\
    \Phi \in \langle\Psi\rangle \\
    \hline
    A \rightarrow f[\bullet\overrightarrow{B}];\Phi
  \end{array}
\]

Существуют и другие пакеты, которые также предоставляют функциональность правил вывода, например:semanticилиproofs.

Answer 2

Я нашелmathpartirpackage самый простой в использовании для набора правил вывода в этом стиле. Стиль по умолчанию — бок о бок антецеденты, но вы можете разместить их на отдельных строках, поместив два переноса строк между антецедентами. В этом случае

\[
\inferrule{A \rightarrow f[\overrightarrow{B}]:= \Psi \\
\Phi \in \langle\Psi\rangle}
          {A \rightarrow f[\bullet\overrightarrow{B}];\Phi}
\]

который будет выглядеть как