乳胶自然演绎

Question

我是 Latex 的新手，我想做自然推理。我知道互联网上有很多资源，这里也经常提到这一点，但我找不到方便、易于使用的软件包或任何其他使用 Latex 进行自然推理的方法。我希望我的证明只有垂直线（没有水平线）并添加我自己的理由，而不是一组预定义的理由。为了更好地说明我的问题，这里有一张图片：

Answer 1

这提供了一个足够的开始；在内部设置构造array（可能带有嵌套）：

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
  \refstepcounter{enumi}(\theenumi)%
  \IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
  \setcounter{enumi}{0}% Restart "logic" counter
  \makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

\[
  \begin{array}{c}
    \logictitle{A / B \rightarrow A} \\[\jot]
    \begin{array}{c | l | l @{\qquad} l }
       \logicstep[first] & \multicolumn{3}{l}{A} \\
      \logicstep[second] & & B & \text{Supp $/~\rightarrow$ Int} \\
       \logicstep[third] & & A & \text{reit \eqref{first}} \\
              \logicstep & \multicolumn{1}{l}{B \rightarrow A} & & \text{$\rightarrow$ Int $\eqref{second} - \eqref{third}$}
    \end{array}
  \end{array}
\]

\end{document}

\logicstep[<label>]设置第一列的编号。可选的<label>允许您\ref对其进行排序（使用\eqref或其他方式）。

---

下面是另一个视觉效果：

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
  \refstepcounter{enumi}(\theenumi)%
  \IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
  \setcounter{enumi}{0}% Restart "logic" counter
  \makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

\[
  \begin{array}{c}
    \logictitle{A / C \rightarrow (B \rightarrow A)} \\[\jot]
    \begin{array}{c | l | l | l @{\qquad} l }
       \logicstep[first] & \multicolumn{3}{l}{A} & \multicolumn{1}{@{}l}{\text{premise}} \\
      \logicstep[second] & \quad & \multicolumn{1}{|l}{C} & \multicolumn{1}{l}{} & \text{Supp, $\rightarrow$ Int} \\
       \logicstep[third] &       &   & B                    & \text{Supp, $\rightarrow$ Int} \\
      \logicstep[fourth] &       &   & A                    & \text{Reit \eqref{first}} \\
       \logicstep[fifth] &       & \multicolumn{1}{|l}{B} & \multicolumn{1}{l}{} & \text{$\rightarrow$ Int, \eqref{third}--\eqref{fourth}} \\
              \logicstep & \multicolumn{3}{l}{C \rightarrow (B \rightarrow A)} & \text{$\rightarrow$ Int, \eqref{second}--\eqref{fifth}}
    \end{array}
  \end{array}
\]

\end{document}

---

现在有一个换行符：

\documentclass{article}

\usepackage{xparse,amsmath}

\makeatletter
\NewDocumentCommand{\logicstep}{ o }{%
  \refstepcounter{enumi}(\theenumi)%
  \IfValueT{#1}{\ltx@label{#1}}%
}
\makeatother

\newcommand{\logictitle}[1]{%
  \setcounter{enumi}{0}% Restart "logic" counter
  \makebox[.5\linewidth][l]{$#1$}%
}

\begin{document}

\[
  \begin{array}{c}
    \logictitle{A / C \rightarrow (B \rightarrow A)} \\[\jot]
    \begin{array}{c | l | l | l @{\qquad} l }
        \logicstep[first] & \multicolumn{3}{l}{A} & \multicolumn{1}{@{}l}{\text{premise}} \\
       \logicstep[second] & \quad & \multicolumn{1}{|l}{C} & \multicolumn{1}{l}{} & \text{Supp, $\rightarrow$ Int} \\
        \logicstep[third] &       &   & B                    & \text{Supp, $\rightarrow$ Int} \\
       \logicstep[fourth] &       &   & A                    & \text{Reit \eqref{first}} \\
                          &       \\[-.8\normalbaselineskip]
        \logicstep[fifth] &       &   & B                    & \text{Example 1} \\
        \logicstep[sixth] &       &   & A                    & \text{Example 2} \\
      \logicstep[seventh] &       & \multicolumn{1}{|l}{B} & \multicolumn{1}{l}{} & \text{$\rightarrow$ Int, \eqref{third}--\eqref{fourth}} \\
               \logicstep & \multicolumn{3}{l}{C \rightarrow (B \rightarrow A)} & \text{$\rightarrow$ Int, \eqref{second}--\eqref{fifth}}
    \end{array}
  \end{array}
\]

\end{document}