☰

Alinear reglas de prueba en tablas

tag-icon • tag-icon tables logic bussproofs
Alinear reglas de prueba en tablas

Me gustaría mostrar las siguientes reglas en una tabla:

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

Ahora mismo parece un poco desordenado. ¡Pero no sé cómo insertar entornos de prueba en tablas!

Respuesta1

Puede colocar árboles de prueba tabularsiempre que los utilice \DisplayProofen lugar de en el prooftreeentorno completo.

La construcción \begin{prooftree}<statements>\end{prooftree}es esencialmente equivalente a

\[
<statements>
\DisplayProof
\]

Aquí está el código que propongo (no toqué el código en el \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}

ingrese la descripción de la imagen aquí

Respuesta2

Estructurar el contenido de un marco en bloques. Agregue, por ejemplo, las siguientes definiciones a su 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

Utilice el blockentorno de la siguiente manera:

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

Además, como se describe en el apartado 2.1 de la documentación de bussproofs, puedes utilizar \DisplayProof(o \DP, si activas los atajos) para componer la prueba, como alternativa al prooftreeentorno. La ventaja es que la prueba resultante \Displayprooftambién se puede poner en un archivo tabular.

ingrese la descripción de la imagen aquí

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

información relacionada