☰

Alinhando regras de prova em tabelas

tag-icon • tag-icon tables logic bussproofs
Alinhando regras de prova em tabelas

Gostaria de exibir as seguintes regras em uma tabela:

\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}

No momento parece um pouco confuso. Mas não sei inserir ambientes de prova em tabelas!

Responder1

Você pode colocar árvores de prova tabulardesde que use, \DisplayProofem vez do prooftreeambiente completo.

A construção \begin{prooftree}<statements>\end{prooftree}é essencialmente equivalente a

\[
<statements>
\DisplayProof
\]

Aqui está o código que proponho (não toquei no código \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}

insira a descrição da imagem aqui

Responder2

Estruture o conteúdo de um quadro em blocos. Adicione, por exemplo, as seguintes definições ao seu preâmbulo.

\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

Use o blockambiente da seguinte forma:

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

Além disso, conforme descrito na seção 2.1 da documentação do bussproofs, você pode usar \DisplayProof(ou \DP, se ativar os atalhos) para compor a prova, como alternativa ao prooftreeambiente. A vantagem é que a prova resultante \Displayprooftambém pode ser colocada em um arquivo tabular.

insira a descrição da imagem aqui

\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}

informação relacionada