편집하다

Question

내가 달성하려는 것은 다음과 같습니다.

1.r                             (Given)
2.(t ∧ r) → s                   (Given)
3.(p → t) → (q → ¬s)            (Given)
    4.t ∧ r                     (Assumption)

내가 얻은 것은 다음과 같습니다.

여기 내 코드가 있습니다

\documentclass[11pt]{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}
    \begin{align*}
    &1. r& &&\text{(Given)}\\
    &2. (t \land r) \imp s&  &&\text{(Given)}\\
    &3. (p \imp t) \imp (q \imp \neg s)& &&\text{(Given)}\\
    &&4. t \land r& &&\text{(Assumption)}
    \end{align*}
\end{proof}

\end{document}

문제:

형식증명에서 들여쓰기는 어떻게 하나요? 오른쪽의 텍스트가 완벽하게 정렬되지 않아도 괜찮지만 들여쓰기를 올바르게 하고 싶습니다. 위 코드에서 생성된 들여쓰기가 너무 큽니다.

아시다시피 저는 LaTex를 처음 접했습니다. 어떤 제안이라도 감사하겠습니다. 이런 종류의 패키지가 있으면 좋을 것 같습니다.

감사해요!

편집하다

완전한 형식적 증명은 다음과 같습니다:

1.r                             (Given)
2.(t ∧ r) → s                   (Given)
3.(p → t) → (q → ¬s)            (Given)
    4.t ∧ r                     (Assumption)
    5.t                         (From 4)
    6.s                         (From 2, 4)
        7. (p → t)              (Assumption)
        8. p                    (From 5, 7)
        ...
    ...
...

Answer 1

당신은 이런 일을 할 수 있습니다

\documentclass{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\newenvironment{level}%
{\addtolength{\itemindent}{2em}}%
{\addtolength{\itemindent}{-2em}}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}\leavevmode
    \begin{enumerate}
    \item $r$ \hfill(Given)
    \begin{level}
    \item $(t \land r) \imp s$ \hfill (Given)
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
      \begin{level}
        \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
        \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
      \end{level}
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
    \end{level}
    \item $t \land r$ \hfill (Assumption)
    \end{enumerate}
\end{proof}

\end{document}

이 경우 환경은 level목록의 항목 들여쓰기를 늘리고 자동으로 줄입니다. 크기 를 변경하여 길이를 변경할 수 있습니다 2em.

Answer 2

당신은 사용할 수 enumerate있습니다enumitem

\documentclass[11pt]{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\usepackage{enumitem}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}\leavevmode
    \begin{enumerate}[ref=\arabic*]
    \item $r$ \hfill(Given)
    \item $(t \land r) \imp s$ \hfill (Given)\label{enum:second}
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
    \begin{enumerate}[start=4,label=\arabic*.,ref=\arabic*]
    \item $t \land r$ \hfill (Assumption)\label{enum:fourth}
    \item $t$ \hfill         (From~\ref{enum:fourth})\label{enum:fifth}
    \item $s$ \hfill          (From~\ref{enum:second},~\ref{enum:fourth})
    \begin{enumerate}[start=7,label=\arabic*.,ref=\arabic*]
    \item $(p \imp t)$ \hfill   (Assumption)\label{enum:seventh}
     \item $p$  \hfill          (From~\ref{enum:fifth},~\ref{enum:seventh})
    \end{enumerate}
    \end{enumerate}
    \end{enumerate}
\end{proof}

\end{document}

참고용으로 메커니즘을 \label사용 했음을 참고하시기 바랍니다 . \ref거리를 더 조정하려면 enumitem패키지 설명서(www.texdoc.net에서 사용 가능) 를 참조하세요.

Answer 3

이런 종류의 증명을 조판하기 위해 설계된 패키지를 사용하는 것이 가장 좋을 것이라고 생각합니다. lplfitch아마도 가장 가깝습니다. 범위를 표시하는 규칙을 그리지만 의 도움으로 이러한 규칙을 제거할 수 있습니다 etoolbox. 다음은 \fitchprf증명 기간 동안 규칙이 0pt를 갖도록 기본 증명 명령을 패치합니다 . 테이블 형식의 규칙 너비는 마지막에 복원됩니다.

lplfitch또한 그러한 교정본의 조판을 쉽게 하기 위해 고안된 다양한 기능을 제공합니다. 예를 들어, 적절한 간격으로 논리적 기호의 범위를 정의합니다. (자세한 내용은 설명서를 참조하세요.)

\documentclass[11pt]{article}
\usepackage{mathtools,amsthm,amssymb}
\usepackage{lplfitch}
\usepackage{etoolbox}
\newlength\savearrayrulewidth
\setlength\savearrayrulewidth{\arrayrulewidth}
\pretocmd{\fitchprf}{\setlength{\arrayrulewidth}{0pt}}{\typeout{Great!}}{\typeout{Oh, no!}}
\apptocmd{\fitchprf}{\setlength{\arrayrulewidth}{\savearrayrulewidth}}{\typeout{Great!}}{\typeout{Oh, no!}}
\begin{document}

\fitchprf{%
  \pline[1]{r}[(Given)]\\
  \pline[2]{(t \land r) \lif s}[(Given)]\\
  \pline[3]{(p \lif t) \lif (q \lif \lnot s)}[(Given)]
}{%
  \subproof{%
    \pline[4]{t \land r}[(Assumption)]
  }{%
  }\\
}

\end{document}

편집하다

또한 이것이 유용한지 여부는 사용하는 시스템에 따라 다르지만 패키지도 다양한 종류의 정당성을 제공합니다. 예를 들어, 증명을 조금 계속하면 다음과 같습니다.

\fitchprf{%
  \pline[1]{r}[(Given)]\\
  \pline[2]{(t \land r) \lif s}[(Given)]\\
  \pline[3]{(p \lif t) \lif (q \lif \lnot s)}[(Given)]
}{%
  \subproof{%
    \pline[4]{t \land r}[(Assumption)]
  }{%
    \pline[5]{s}[\life{2}{4}]\\
    \pline[6]{t}[\lande{5}]\\
    \subproof{%
      \pline[7]{p \lif t}[(Assumption)]
    }{%
      \pline[8]{q \lif \lnot s}[\life{3}{7}]
    }
  }\\
}

생산하다