2/19
\begin{frame}
  \frametitle{ProofWeb}

  \begin{goal}{}
    ProofWeb allows to practise natural deduction online:
    \begin{itemize}
    \medskip
      \item based on the proof assistant Coq
    \medskip
      \item the derivations are automatically checked for correctness
    \medskip
    \end{itemize}
  \end{goal}
  
\end{frame}