Check-in [a01b5086af]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Updated presentation: final version.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | trunk
Files: files | file ages | folders
SHA1:a01b5086af28f43accd9ed904d2d5ec1f9d3d8a6
User & Date: andy 2015-05-07 09:54:24
Context
2015-05-07
09:54
Updated presentation: final version. Leaf check-in: a01b5086af user: andy tags: trunk
2015-05-01
09:12
Added an index page to the server, so you can browse http://localhost:4001 and get nice links to the examples. check-in: 3bb6b9ecdb user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

    85     85   
    86     86   
    87     87   \begin{frame}\frametitle{Paper proofs}
    88     88   
    89     89   Paper proofs are common, but problematic for education:
    90     90   \begin{itemize}
    91     91   \item Too flexible; allow a wide variety of ``almost correct'' answers.
    92         -\item Delayed results; turn in a proof assignment, get results back a week
           92  +\item \pause Delayed results; turn in a proof assignment, get results back a week
    93     93       later. \pause \alert{Batch processing for proofs.} 
    94     94   \item \pause Non-interactive.
    95     95   \end{itemize}
    96     96   
    97     97   \end{frame}
    98     98   
    99     99   
................................................................................
   456    456   \end{frame}
   457    457   
   458    458   \begin{frame}\frametitle{\texttt{subst} module}
   459    459   
   460    460   The \texttt{subst} module implements:
   461    461   \begin{itemize}
   462    462   \item Custom variable type (encoded as special atoms)
   463         -\item Robinson unification algorithm over term containing these variables
          463  +\item Robinson unification algorithm over terms containing these variables
   464    464   \item Application of substitutions to terms
   465    465   \end{itemize}
   466    466   
   467    467   \end{frame}
   468    468   
   469    469   \begin{frame}\frametitle{\texttt{program} module}
   470    470   
................................................................................
   555    555   \item Variables in scope
   556    556   \end{itemize}
   557    557   
   558    558   \end{frame}
   559    559   
   560    560   \begin{frame}\frametitle{Proof checking, cont.}
   561    561   
   562         -Substitutions and variable bindings flow through the tree nontrially:
          562  +Substitutions and variable bindings flow through the tree nontrivially:
   563    563   \vfill
   564    564   \begin{itemize}
   565    565   \item Substitutions flow from leaves to root, but also left-to-right in 
   566    566     conjunctions.
   567    567   \item Variable scopings flow from root to leaves, but also left-to-right in
   568    568     conjunctions.
   569    569   \end{itemize}
................................................................................
   573    573   
   574    574   \end{frame}
   575    575   
   576    576   \begin{frame}\frametitle{Proof construction procedure}
   577    577   
   578    578   \begin{enumerate}
   579    579   \item User selects an element (antecedent or consequent) in the current proof
   580         -  state. Path to the element along with the proof tree is passed to the server.
          580  +  state. 
   581    581   \item Path to the element along with the proof tree is passed to the server.
   582    582   \item Server calls \texttt{checker:elaborate} to elaborate the desired element.
   583    583   \item Elaborated proof is returned to client.
   584    584   \item New proof is checked for completeness. Complete? then \textsc{Stop}, else
   585    585     \textsc{GoTo} 1.
   586    586   \end{enumerate}
   587    587