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