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 Unified Diffs Ignore Whitespace Patch

Changes to presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
...
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
...
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
...
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587


\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
    later. \pause \alert{Batch processing for proofs.} 
\item \pause Non-interactive.
\end{itemize}

\end{frame}


................................................................................
\end{frame}

\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 Application of substitutions to terms
\end{itemize}

\end{frame}

\begin{frame}\frametitle{\texttt{program} module}

................................................................................
\item Variables in scope
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Proof checking, cont.}

Substitutions and variable bindings flow through the tree nontrially:
\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
  conjunctions.
\end{itemize}
................................................................................

\end{frame}

\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.
\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.
\end{enumerate}








|







 







|







 







|







 







|







85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
...
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
...
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
...
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587


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


................................................................................
\end{frame}

\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 terms containing these variables
\item Application of substitutions to terms
\end{itemize}

\end{frame}

\begin{frame}\frametitle{\texttt{program} module}

................................................................................
\item Variables in scope
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Proof checking, cont.}

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
  conjunctions.
\end{itemize}
................................................................................

\end{frame}

\begin{frame}\frametitle{Proof construction procedure}

\begin{enumerate}
\item User selects an element (antecedent or consequent) in the current proof
  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.
\end{enumerate}