☰

用于自然演绎的逻辑证明虚线框

tag-icon • tag-icon tables logic
用于自然演绎的逻辑证明虚线框

我一直在使用Logicproof用 Fitch 风格编写证明的包。它使用表格创建环境，使编写证明变得不那么麻烦。

我似乎无法弄清楚如何在子证明中创建虚线框，如本例所示：

自然演绎示例

这是我目前所得到的。然而，第二个子证明应该使用虚线框。

\documentclass{article}
\usepackage{logicproof}
\usepackage{amssymb}

\begin{document}

\begin{logicproof}{2}
    \begin{subproof}
        \square p \land \square q & assumption\\
        \square p & $\land \mathrm{e}_1$ 1\\
        \square q & $\land \mathrm{e}_2$ 1\\
        \begin{subproof} %This should have a dashed box
            p & $\square \mathrm{e}$ 2\\
            q & $\square \mathrm{e}$ 3\\
            p \land q & $\land \mathrm{i}$ 4, 5
        \end{subproof}
        \square (p \land q) & $\square \mathrm{i}$ 4--6
    \end{subproof}
    \square p \land \square q \to \square (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}

\end{document}

有人知道是否可以使用 logicproof 创建虚线子证明吗？

如果这不可能的话，如何创建类似于子证明环境的环境？

答案1

由于近一个月内没有人回答这个问题，我将发布我的部分解决方案，希望其他人能够接受挑战。

该程序包基本上使用tabular环境来构建证明。它用于\cline绘制水平线。因此，如果我们可以替换虚线，我们就可以完成一半的问题。

arydshlntabular在和环境中支持虚线水平和垂直规则array。因此我们可以用其替代\cdashline{}标准的\cline{}。

logicproof我们通过修改的命令副本\lp@cr@clines（我们称之为）和修改的环境\lp@cr@cdashlines副本（我们称之为）来实现这一点。使用其中使用，并使用其中使用。logicproofsubproofsubproofdsubproofd\lp@cr@cdashlinessubproof\lp@cr@clines\lp@cr@cdashlines\cdashline{}\lp@cr@clinescline{}

这样做的结果是，我们可以使用subproofd来subproof排版一个子证明，其框的水平线是虚线而不是连续的。

半虚线框

显然，剩下的问题就是让框的垂直线变成虚线。问题在于通过提供for /规范arydshln的替代方案来支持垂直虚线规则。|tabulararray

但logicproof并不使用这种机制来绘制其框的垂直线，正如其标准列规范所示：

 {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}

相反，它使用\vline，我不知道如何制作这些在环境中冲破subproofd。

\documentclass{article}
\usepackage{logicproof}
\usepackage{arydshln}
\usepackage{amssymb}
\newcommand*{\nec}{\ensuremath{\mathord{\square}}}
\makeatletter
\newcommand{\lp@cr@cdashlines}{% modified copy of lp@cr@clines
  \lp@set@clines%
  \lp@orig@arraycr%
  \cdashline{\value{lp@cline@1}-\value{lp@cline@2}}%
}
\newenvironment{subproofd}{% modified copy of subproof
  \ifthenelse{%
    \value{lp@total@nests}>\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Too many nested subproofs!}{%
      Increase the maximum number of nested subproofs allowed
      in the current logicproof environment.%
    }%
  }%
  \endgroup%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
  \lp@add@space%
  \lp@go@up@a@line%
  \stepcounter{lp@nested}%
  \lp@cr@cdashlines%
  &%
  \lp@continue@proof@line%
}{%
  \ifthenelse{%
    0<\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Cannot end a subproof before it begins}{%
      You must have a \protect\begin{subproof} before you can use %
      \protect\end{subproof}.%
    }%
  }%
  \lp@stop@proof@line%
  \lp@cr@cdashlines%
  \addtocounter{lp@nested}{-1}%
  \lp@extend@space%
  \lp@start@proof@line%
  \begingroup%
  \def\@currenvir{subproofd}%
}
\makeatother
\begin{document}

\begin{logicproof}{2}
    \begin{subproof}
        \nec p \land \nec q & assumption\\
        \nec p & $\land \mathrm{e}_1$ 1\\
        \nec q & $\land \mathrm{e}_2$ 1\\
        \begin{subproofd} %This should have a dashed box
            p & $\nec \mathrm{e}$ 2\\
            q & $\nec \mathrm{e}$ 3\\
            p \land q & $\land \mathrm{i}$ 4, 5
        \end{subproofd}
        \nec (p \land q) & $\nec \mathrm{i}$ 4--6
    \end{subproof}
    \nec p \land \nec q \to \nec (p \land q) & $\to \mathrm{i}$ 1--7
\end{logicproof}

\end{document}

相关内容