\begin{frame}{Satisfiability in Propositional Logic}
  A formula of propositional logic consists of
  \begin{talign}
    \texttt{true} && 
    \text{conjunction } \wedge &&
    \text{variables} \\
    \texttt{false} &&
    \text{disjunction } \vee 
    &&
    \text{negation } \neg 
  \end{talign}\vspace{-3ex}
  
  \begin{goal}{}
    A formula of propositional logic $\phi$ is \emph{satisfiable} if there exists
    an assignment of \texttt{true} and \texttt{false} to the variables
    such that $\phi$ evaluates to \texttt{true}.
  \end{goal}
  \pause\medskip
  
  \begin{block}{Theorem}
    Satisfiability of formulas of propositional logic is in NP.
  \end{block}
  \pause
  
  \begin{proof}
    We can construct a nondeterministic Turing machine that
    \begin{itemize}
      \item guesses an assignment of \texttt{true} and \texttt{false} to the variables,
      \item evaluates the formula (in polynomial time), and
    \end{itemize}
    accepts if the evaluation is \texttt{true}.
  \end{proof}
\end{frame}