自然演繹のための論理証明破線ボックス

Question

ほぼ 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}

Answer 1