☰

테이블의 증명 규칙 정렬

tag-icon • tag-icon tables logic bussproofs
테이블의 증명 규칙 정렬

다음 규칙을 표에 표시하고 싶습니다.

\documentclass[10pt]{beamer}
% Proofs
\usepackage{bussproofs}

\begin{document}

\begin{frame}{$\mathcal{M}$}
\textbf{Inference rules}
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{prooftree}
\AxiomC{[$\phi$]}
\noLine
\UnaryInfC{$\psi$}
\LeftLabel{$\Rightarrow$-intro}
\UnaryInfC{$\phi \Rightarrow \psi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\phi \Rightarrow \psi$}
    \AxiomC{$\phi$}
    \LeftLabel{$\Rightarrow$-elim}
    \BinaryInfC{$\phi \Rightarrow \psi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
    \LeftLabel{$\bigwedge$-intro}
    \UnaryInfC{$\bigwedge x. \phi$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\bigwedge x. \phi$}
    \LeftLabel{$\bigwedge$-elim}
    \UnaryInfC{$\phi[b/x]$}
\end{prooftree}
\end{column}

\begin{column}{0.5\textwidth}
\begin{prooftree}
    \AxiomC{}
    \LeftLabel{Refl}
    \UnaryInfC{$a \equiv a$}
\end{prooftree}
    
\begin{prooftree}
    \AxiomC{$a \equiv b$}
    \LeftLabel{Symmetry}
    \UnaryInfC{$b \equiv a$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$a \equiv b$}
    \AxiomC{$b \equiv c$}
    \LeftLabel{Transitivity}
    \BinaryInfC{$a \equiv c$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$y \notin fv(a)$}
    \LeftLabel{$\alpha$-conversion}
    \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{}
    \LeftLabel{$\beta$-conversion}
    \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$x \notin fv(f)$}
    \LeftLabel{$\eta$-conversion}
    \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
\end{prooftree}

\note{
\begin{itemize}
\item $\eta$-conversion is equivalent to extensionality:

\begin{prooftree}
    \AxiomC{$f(x) \equiv g(x)$}
    \UnaryInfC{$f \equiv g$}
\end{prooftree}

\item It holds when $x \notin fv(f,g, \text{assumps})$.
\end{itemize}

\begin{itemize}
\item The side condition in $\bigwedge$-intro is better understood with a more verbose rule:

\begin{prooftree}
    \AxiomC{$\Gamma \vdash \varphi(y)$}
    \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
    \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
\end{prooftree}

\item Recall that $\bigwedge x. \varphi$ is an abbreviation of $\bigwedge (\lambda x. \varphi)$. So both formulations are equal. 
\end{itemize}
}
\end{column}
\end{columns}
\end{frame}

\end{document}

지금은 조금 지저분해 보입니다. 하지만 테이블에 증명 환경을 삽입하는 방법을 모르겠습니다!

답변1

전체 환경이 아닌 tabular사용하는 경우 증거 나무를 배치할 수 있습니다 .\DisplayProofprooftree

구성은 \begin{prooftree}<statements>\end{prooftree}본질적으로 다음과 같습니다.

\[
<statements>
\DisplayProof
\]

제가 제안하는 코드는 다음과 같습니다( 의 코드는 건드리지 않았습니다 \note).

\documentclass[10pt]{beamer}
% Proofs
\usepackage{bussproofs}
% tables
\usepackage{booktabs}

\begin{document}

\begin{frame}{$\mathcal{M}$}
\textbf{Inference rules}

\medskip

\begin{columns}
\begin{column}[t]{0.5\textwidth}
\centering
\begin{tabular}[t]{@{}l@{}}
\toprule[0pt] % set the anchor
  \AxiomC{[$\phi$]}
  \noLine
  \UnaryInfC{$\psi$}
  \LeftLabel{$\Rightarrow$-intro}
  \UnaryInfC{$\phi \Rightarrow \psi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\phi \Rightarrow \psi$}
  \AxiomC{$\phi$}
  \LeftLabel{$\Rightarrow$-elim}
  \BinaryInfC{$\phi \Rightarrow \psi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
  \LeftLabel{$\bigwedge$-intro}
  \UnaryInfC{$\bigwedge x. \phi$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$\bigwedge x. \phi$}
  \LeftLabel{$\bigwedge$-elim}
  \UnaryInfC{$\phi[b/x]$}
  \DisplayProof
\end{tabular}
\end{column}

\begin{column}[t]{0.5\textwidth}
\begin{tabular}[t]{@{}l@{}}
\toprule[0pt] % set the anchor
  \AxiomC{}
  \LeftLabel{Refl}
  \UnaryInfC{$a \equiv a$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$a \equiv b$}
  \LeftLabel{Symmetry}
  \UnaryInfC{$b \equiv a$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$a \equiv b$}
  \AxiomC{$b \equiv c$}
  \LeftLabel{Transitivity}
  \BinaryInfC{$a \equiv c$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$y \notin fv(a)$}
  \LeftLabel{$\alpha$-conversion}
  \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{\vphantom{X}}
  \LeftLabel{$\beta$-conversion}
  \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
  \DisplayProof
\\ \addlinespace \midrule \addlinespace
  \AxiomC{$x \notin fv(f)$}
  \LeftLabel{$\eta$-conversion}
  \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
  \DisplayProof
\end{tabular}

\note{
\begin{itemize}
\item $\eta$-conversion is equivalent to extensionality:

\begin{prooftree}
    \AxiomC{$f(x) \equiv g(x)$}
    \UnaryInfC{$f \equiv g$}
\end{prooftree}

\item It holds when $x \notin fv(f,g, \text{assumps})$.
\end{itemize}

\begin{itemize}
\item The side condition in $\bigwedge$-intro is better understood with a more verbose rule:

\begin{prooftree}
    \AxiomC{$\Gamma \vdash \varphi(y)$}
    \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
    \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
\end{prooftree}

\item Recall that $\bigwedge x. \varphi$ is an abbreviation of $\bigwedge (\lambda x. \varphi)$. So both formulations are equal. 
\end{itemize}
}
\end{column}
\end{columns}
\end{frame}

\end{document}

여기에 이미지 설명을 입력하세요

답변2

프레임의 내용을 블록으로 구성합니다. 예를 들어 서문에 다음 정의를 추가하세요.

\setbeamercolor{block title}{use=structure,fg=structure.fg,bg=structure.fg!30!bg}
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!60!bg}
\setbeamertemplate{blocks}[rounded][shadow]
\setbeamertemplate{navigation symbols}{} % removes the navigation symbols that nobody uses

다음과 같이 환경을 사용하십시오 block.

\begin{block}{Headline of block, may be empty}
  Part of the contents of the frame
\end{block}

또한 문서의 섹션 2.1에 설명된 대로 환경에 대한 대안으로 (또는 단축키를 활성화하는 경우)를 bussproofs사용하여 교정을 조판할 수 있습니다 . 장점은 결과로 나온 증명 을 .\DisplayProof\DPprooftree\Displayprooftabular

여기에 이미지 설명을 입력하세요

\documentclass[10pt]{beamer}
\setbeamercolor{block title}{use=structure,fg=structure.fg,bg=structure.fg!30!bg}
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!60!bg}
\setbeamertemplate{blocks}[rounded][shadow]
\setbeamertemplate{navigation symbols}{}
%Proofs
\usepackage{bussproofs}

\begin{document}

\begin{frame}{$\mathcal{M}$~-- Inference rules}
\begin{columns}
  \begin{column}{0.45\textwidth}
    \begin{block}{Implication}
      \begin{tabular}{@{}lc@{}}
        $\Rightarrow$-intro
      & \AxiomC{[$\phi$]} \noLine \UnaryInfC{$\psi$}
        \LeftLabel{}
        \UnaryInfC{$\phi \Rightarrow \psi$}
        \DisplayProof
      \\[5ex]
        $\Rightarrow$-elim
      & \AxiomC{$\phi \Rightarrow \psi$} \AxiomC{$\phi$}
        \LeftLabel{}
        \BinaryInfC{$\phi \Rightarrow \psi$}
        \DisplayProof           
      \end{tabular}
    \end{block}

    \begin{block}{Quantification}
      \begin{tabular}{@{}lc@{}}
        $\bigwedge$-intro
      & \AxiomC{$\phi$ \; $x \notin fv(\text{assumps})$}
        \UnaryInfC{$\bigwedge x. \phi$}
        \DisplayProof                    
      \\[5ex]
        $\bigwedge$-elim
      & \AxiomC{$\bigwedge x. \phi$}
        \UnaryInfC{$\phi[b/x]$}
        \DisplayProof                    
      \end{tabular}
    \end{block}
\end{column}

\begin{column}{0.54\textwidth}
  \begin{block}{Equivalence}
    \begin{tabular}{@{}lc@{}}
      reflexivity
    & \AxiomC{}
      \UnaryInfC{$a \equiv a$}
      \DisplayProof
    \\[3ex]
      symmetry
    & \AxiomC{$a \equiv b$}
      \UnaryInfC{$b \equiv a$}
      \DisplayProof
    \\[3ex]
      transitivity
    & \AxiomC{$a \equiv b$}
      \AxiomC{$b \equiv c$}
      \BinaryInfC{$a \equiv c$}
      \DisplayProof
    \end{tabular}
  \end{block}
  \begin{block}{$\lambda$ rules}
    \begin{tabular}{@{}lc@{}}
      $\alpha$-conversion
    & \AxiomC{$y \notin fv(a)$}
      \UnaryInfC{$(\lambda x. a) \equiv (\lambda y. a[y/x])$}
      \DisplayProof
    \\[4ex]
      $\beta$-conversion
    & \AxiomC{}
      \UnaryInfC{$(\lambda x. a)b \equiv a[b/x]$}
      \DisplayProof
    \\[3ex]
      $\eta$-conversion
    & \AxiomC{$x \notin fv(f)$}
      \UnaryInfC{$(\lambda x. f(x)) \equiv f$}
      \DisplayProof
    \end{tabular}
  \end{block}
  \note{
    \begin{itemize}
    \item $\eta$-conversion is equivalent to extensionality:

      \begin{prooftree}
        \AxiomC{$f(x) \equiv g(x)$} \UnaryInfC{$f \equiv g$}
      \end{prooftree}

    \item It holds when $x \notin fv(f,g, \text{assumps})$.
    \end{itemize}

    \begin{itemize}
    \item The side condition in $\bigwedge$-intro is better understood
      with a more verbose rule:

      \begin{prooftree}
        \AxiomC{$\Gamma \vdash \varphi(y)$}
        \RightLabel{$y \notin fv(\Gamma) \land x \notin fv(\varphi)$}
        \UnaryInfC{$\Gamma \vdash \forall x. \varphi(x)$}
      \end{prooftree}

    \item Recall that $\bigwedge x. \varphi$ is an abbreviation of
      $\bigwedge (\lambda x. \varphi)$. So both formulations are
      equal.
    \end{itemize}
  }
\end{column}
\end{columns}
\end{frame}

\end{document}

관련 정보