☰

Логически защищенные пунктирные поля для естественной дедукции

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}

Кто-нибудь знает, можно ли создать пунктирное поддоказательство с помощью logicproof?

Если это невозможно, как можно создать среду, подобную субустойчивой?

решение1

Поскольку никто не ответил на этот вопрос уже почти месяц, я собираюсь опубликовать свое частичное решение в надежде, что кто-то еще примет вызов.

Пакет использует tabularсреду, в основном, для построения доказательства. Он использует ее \clineдля рисования горизонтальных линий. Так что, если мы сможем заменить пунктирные линии, мы сможем решить половину проблемы.

arydshlnподдерживает горизонтальные и вертикальные пунктирные линии в средах tabularи array. Поэтому мы можем заменить его \cdashline{}на стандартный \cline{}.

Мы делаем это, создавая измененную копию logicproofкоманды \lp@cr@clines, которую мы называем \lp@cr@cdashlines, и измененную копию logicproofсреды subproof, которую мы называем subproofd. subproofdиспользует \lp@cr@cdashlines, где subproofиспользует \lp@cr@clines, и \lp@cr@cdashlinesиспользует , \cdashline{}где \lp@cr@clinesиспользует cline{}.

Результатом этого является то, что мы можем использовать subproofdвместо subproofдля набора текста подкорректуру, горизонтальные линии рамки которой являются пунктирными, а не сплошными.

полупунктирная рамка

Очевидно, что оставшаяся проблема — сделать вертикальные линии коробки пунктирными. Проблема в том, что arydshlnподдерживает вертикальные пунктирные правила, предоставляя альтернативу |для спецификаций tabular/ .array

Но 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}

Связанный контент