☰

자연 추론을 위한 논리 증명 점선 상자

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수평선을 그리는 데 사용됩니다 . 따라서 점선으로 대체할 수 있다면 문제의 절반을 해결할 수 있습니다.

arydshlntabular및 환경 에서 점선 가로 및 세로 규칙을 지원합니다 array. 그래서 우리는 그것을 \cdashline{}표준으로 대체할 수 있습니다 \cline{}.

우리 는 호출하는 logicproof명령 의 수정된 복사본 과 호출하는 환경 의 수정된 복사본을 만들어 이를 수행합니다 . 사용 위치 , 사용 위치 사용 .​\lp@cr@clines\lp@cr@cdashlineslogicproofsubproofsubproofdsubproofd\lp@cr@cdashlinessubproof\lp@cr@clines\lp@cr@cdashlines\cdashline{}\lp@cr@clinescline{}

이것의 결과는 상자의 수평선이 연속이 아닌 점선으로 표시된 하위 증명을 조판하기 위해 subproofd대신 사용할 수 있다는 것입니다 .subproof

반 점선 상자

분명히 남은 문제는 상자의 수직선을 점선으로 만드는 것입니다. 문제는 / 사양 에 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}

관련 정보