☰

自然演繹的邏輯證明虛線框

tag-icon • tag-icon tables logic
自然演繹的邏輯證明虛線框

我一直在使用邏輯證明包以 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}

有誰知道是否可以使用邏輯證明來創建虛線子證明？

如果這是不可能的，那麼如何創造一個類似 subproof 環境的環境呢？

答案1

由於近一個月沒有人回答這個問題，我將發布我的部分解決方案，希望其他人能夠接受挑戰。

基本上，該包使用tabular環境來建立證明。它用於\cline繪製水平線。所以，如果我們能用虛線代替，我們就可以解決一半的問題。

arydshlntabular支撐和環境中的虛線水平和垂直規則array。所以我們可以用它\cdashline{}來代替標準\cline{}。

我們透過建立一個修改後的logicproof命令副本\lp@cr@clines（我們稱之為\lp@cr@cdashlines）和一個修改後的logicproof環境副本subproof（我們稱之為）來做到這一點subproofd。在使用的地方subproofd使用，並在使用的地方使用。\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}

相關內容