☰

Beweisregeln in Tabellen ausrichten

tag-icon • tag-icon tables logic bussproofs
Beweisregeln in Tabellen ausrichten

Ich möchte folgende Regeln in einer Tabelle darstellen:

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

Im Moment sieht es etwas chaotisch aus. Aber ich weiß nicht, wie man Beweisumgebungen in Tabellen einfügt!

Antwort1

Sie können Beweisbäume platzieren, tabularsofern Sie diese verwenden, \DisplayProofund nicht die gesamte prooftreeUmgebung.

Die Konstruktion \begin{prooftree}<statements>\end{prooftree}entspricht im Wesentlichen

\[
<statements>
\DisplayProof
\]

Hier ist der Code, den ich vorschlage (ich habe den Code im nicht verändert \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}

Bildbeschreibung hier eingeben

Antwort2

Strukturieren Sie den Inhalt eines Frames in Blöcke. Fügen Sie Ihrer Präambel beispielsweise die folgenden Definitionen hinzu.

\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

Verwenden Sie die blockUmgebung wie folgt:

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

bussproofsDarüber hinaus können Sie , wie in Abschnitt 2.1 der Dokumentation von beschrieben , alternativ zur Umgebung \DisplayProof(oder , wenn Sie die Tastenkombinationen aktivieren) den Beweis setzen . Der Vorteil besteht darin, dass der aus resultierende Beweis auch in ein gesetzt werden kann .\DPprooftree\Displayprooftabular

Bildbeschreibung hier eingeben

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

verwandte Informationen