线性自然演绎

Question

有人知道一个允许用这种笔画以这种线性形式写出自然推理的软件包吗？谢谢！PS ND 的示例来自 Jan von Plato 的书《逻辑推理要素》。

Answer 1

有点晚了，但这里有一个解决方案。这个想法是在环境中的合适位置pstricks添加空节点（ ） ，然后用节点连接将它们连接起来。您可以查看包文档以了解详细信息。\pnodestabular\ncbarpst-node

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fourier}

\usepackage{array}
\usepackage{pstricks-add}
\usepackage{auto-pst-pdf}

\newcommand\lAnd{\mathrel{\&}}

\begin{document}

\begin{postscript}
  \psset{angle=180, linewidth=0.6pt}
  \renewcommand\arraystretch{1.25}
  \newcounter{tabenum}\setcounter{tabenum}{0}
  \newcommand{\tabitem}{\refstepcounter{tabenum} \thetabenum.}
  \begin{tabular}{r@{\enspace}>{$}l<{$}@{\qquad}l}
    \pnode(-0.4em,0.6ex){H1}\tabitem & A\lAnd B & hypothesis: goal $\neg\neg A\lAnd\neg\neg B$ \\
    \tabitem & A & $1,\lAnd E$ \\
    \tabitem & B & $1, \lAnd E$ \\
    \pnode(-0.4em,0.6ex){H2}\tabitem & \neg A & hypothesis: goal $\bot$ \\
    \tabitem & \bot & $4, 1, \subset E$ \\
    \tabitem & \neg\neg A \pnode(0, 2.25ex){G2} & $4{-}5, \subset I$ \\
    \pnode(-0.4em,0.6ex){H3}\tabitem & \neg B & hypothesis: goal $\bot$ \\
    \tabitem & \bot & $7, 3, \subset E$ \\
    \tabitem & \neg\neg B \pnode(0, 2.25ex){G3} & $7{-}8, \subset I$ \\
    \tabitem & \neg\neg A\lAnd\neg\neg B & $6, 9, \lAnd I$ \\
    \tabitem & A\lAnd B \supset \neg\neg A\lAnd\neg\neg B \pnode(0, 2.3ex){G1}
  \end{tabular}%\end{listliketab}
  \ncbar[armA=20pt]{H1}{G1}
  \ncbar{H2}{G2}
  \ncbar{H3}{G3}
\end{postscript}

\end{document}