Check-in [a01b5086af]

Not logged in

Overview
Comment: Updated presentation: final version. Tarball | ZIP archive | SQL archive family | ancestors | trunk files | file ages | folders a01b5086af28f43accd9ed904d2d5ec1f9d3d8a6 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

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}