Index: presentation/arend-presentation.pdf
==================================================================
--- presentation/arend-presentation.pdf
+++ presentation/arend-presentation.pdf
cannot compute difference between binary files
Index: presentation/arend-presentation.tex
==================================================================
--- presentation/arend-presentation.tex
+++ presentation/arend-presentation.tex
@@ -87,11 +87,11 @@
\begin{frame}\frametitle{Paper proofs}
Paper proofs are common, but problematic for education:
\begin{itemize}
\item Too flexible; allow a wide variety of ``almost correct'' answers.
-\item Delayed results; turn in a proof assignment, get results back a week
+\item \pause Delayed results; turn in a proof assignment, get results back a week
later. \pause \alert{Batch processing for proofs.}
\item \pause Non-interactive.
\end{itemize}
\end{frame}
@@ -458,11 +458,11 @@
\begin{frame}\frametitle{\texttt{subst} module}
The \texttt{subst} module implements:
\begin{itemize}
\item Custom variable type (encoded as special atoms)
-\item Robinson unification algorithm over term containing these variables
+\item Robinson unification algorithm over terms containing these variables
\item Application of substitutions to terms
\end{itemize}
\end{frame}
@@ -557,11 +557,11 @@
\end{frame}
\begin{frame}\frametitle{Proof checking, cont.}
-Substitutions and variable bindings flow through the tree nontrially:
+Substitutions and variable bindings flow through the tree nontrivially:
\vfill
\begin{itemize}
\item Substitutions flow from leaves to root, but also left-to-right in
conjunctions.
\item Variable scopings flow from root to leaves, but also left-to-right in
@@ -575,11 +575,11 @@
\begin{frame}\frametitle{Proof construction procedure}
\begin{enumerate}
\item User selects an element (antecedent or consequent) in the current proof
- state. Path to the element along with the proof tree is passed to the server.
+ state.
\item Path to the element along with the proof tree is passed to the server.
\item Server calls \texttt{checker:elaborate} to elaborate the desired element.
\item Elaborated proof is returned to client.
\item New proof is checked for completeness. Complete? then \textsc{Stop}, else
\textsc{GoTo} 1.