Check-in [a24ff57f47]

Not logged in

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

Overview
Comment:Presentation work. Added PDF of presentation.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:a24ff57f473fea7c6319fce2d16f15b424a0bf4c
User & Date: andy 2015-04-22 10:29:38
Context
2015-04-22
10:30
Added material to the report on the handling of explicit quantifiers. Leaf check-in: 8a438a8abd user: andy tags: forall-exists
10:29
Presentation work. Added PDF of presentation. Leaf check-in: a24ff57f47 user: andy tags: trunk
2015-04-21
21:35
Started work on better handling of forall/exists in the reasoning language. Leaf check-in: e8532f2591 user: andy tags: forall-exists
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Added presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

    11     11     \usetheme{Warsaw}
    12     12     % Frankfurt
    13     13   
    14     14     \usecolortheme{beaver}
    15     15     \useinnertheme{circles}
    16     16   
    17     17   
    18         -  \setbeamercovered{transparent}
           18  +  \setbeamercovered{invisible}
    19     19     % or whatever (possibly just delete it)
    20     20   }
    21     21   
    22     22   
    23     23   
    24     24   \usepackage{amsmath} % extended mathematics
    25     25   \usepackage{amssymb}
................................................................................
    27     27   
    28     28   % ???
    29     29   \usepackage[english]{babel}
    30     30   
    31     31   % Make math look a little better
    32     32   \usepackage{eulervm}
    33     33   
    34         -% Use Gill Sans for most text
           34  +% Use Raleway for most text
    35     35   \usepackage{fontspec}
    36     36   \defaultfontfeatures{Mapping=tex-text}
    37         -\setsansfont{Gill Sans MT}
           37  +\setsansfont{Raleway}
    38     38   
    39     39   
    40     40   
    41     41   
    42         -\title{Arend} 
           42  +\title{Arend --- Proof Assistant Assisted Pegagogy} 
    43     43   
    44     44   \subtitle{A graphical proof assistant for undergraduate computer science 
    45     45   education}
    46     46   
    47     47   \author{Andrew V. Clifton}
    48     48   
    49     49   \institute[California State University, Fresno] % (optional, but mostly needed)
................................................................................
    60     60   \begin{document}
    61     61   
    62     62   \begin{frame}
    63     63   \titlepage
    64     64   \end{frame}
    65     65   
    66     66   
    67         -\section{Introduction}
           67  +\section{Background}
           68  +
           69  +
           70  +\begin{frame}\frametitle{Formal proofs}
           71  +
           72  +Formal proofs --- an important component of computer science education.
           73  +
           74  +Prove
           75  +\begin{itemize}
           76  +\item $\forall x,y \in \mathbb{N}: x + y = y + x$.
           77  +\item If $T$ is a complete binary tree with $n = |T|$ nodes, then the height of
           78  +    any node is at most $\lfloor \log_2 n \rfloor$.
           79  +\item The reverse of a regular language $L^\text{r}$ is itself regular.
           80  +\end{itemize}
           81  +
           82  +\end{frame}
           83  +
           84  +
           85  +\begin{frame}\frametitle{Paper proofs}
           86  +
           87  +Paper proofs are common, but problematic:
           88  +\begin{itemize}
           89  +\item Too flexible; allow a wide variety of ``almost correct'' answers.
           90  +\item Delayed results; turn in a proof assignment, get results back a week
           91  +    later. \pause \alert{Batch processing for proofs.} 
           92  +\item \pause Non-interactive.
           93  +\end{itemize}
           94  +
           95  +\end{frame}
           96  +
           97  +
           98  +\begin{frame}\frametitle{Computer-assisted logic}
           99  +
          100  +Using computers to do logic is not a new idea:
          101  +\begin{itemize}
          102  +\item \pause Automated theorem provers (e.g., AUTOMATH)
          103  +\item \pause Model checkers
          104  +\item \pause \alert{Proof assistants} (Abella, Coq, Arend, etc.)
          105  +\end{itemize}
          106  +
          107  +\end{frame}
          108  +
          109  +
          110  +\begin{frame}\frametitle{Proof assistants}
          111  +
          112  +A proof assistant
          113  +\begin{itemize}
          114  +\item \pause \alert{Assists} the user in constructing a \alert{valid} proof.
          115  +\item \pause \alert{Forbids} the construction of \alert{invalid} proofs.
          116  +\item \pause Presents proofs, complete or not, to the user in a comprehensible
          117  +    format.
          118  +\end{itemize}
          119  +
          120  +\end{frame}
          121  +
          122  +\begin{frame}\frametitle{Proof assistants, cont.}
          123  +
          124  +Some well-known proof assistants:
          125  +\begin{itemize}
          126  +\item Twelf (previously used in CSCI 217)
          127  +\item Coq
          128  +\item Abella (currently used in CSCI 217)
          129  +\item Agda
          130  +\end{itemize}
          131  +
          132  +\end{frame}
          133  +
          134  +
          135  +\begin{frame}\frametitle{Aside: the Curry-Howard Isomorphism}
          136  +
          137  +An aside:
          138  +
          139  +Some proof assistants bridge the gap between functional programming and proofs,
          140  +thanks to the \alert{Curry-Howard isomorphism}.
          141  +
          142  +\begin{definition}
          143  +The Curry-Howard isomorphism states that \emph{proofs} are to \emph{propositions}
          144  +as \emph{programs} are to \emph{types}.
          145  +\end{definition}
          146  +
          147  +$a : A$ can mean ``$a$ is a program with type $A$'', or ``$a$ is a proof of the 
          148  +proposition $A$''.
          149  +
          150  +\end{frame}
          151  +
          152  +\begin{frame}\frametitle{Curry-Howard isomorphism, cont.}
          153  +
          154  +Some examples:
          155  +\begin{itemize}
          156  +\item If $p : P$ and $q : Q$ then the pair $(p,q) : P \land Q$.
          157  +\item If $p : P$ and $q : Q$ then either $\mathsf{left}(p) : P \lor Q$ or
          158  +    $\mathsf{right}(q) : P \lor Q$.
          159  +\item The most interesting: $P -> Q$ means ``$P$ implies $Q$''. \pause But it
          160  +    is also the type of \alert{functions} from $P$ to $Q$. A proof of 
          161  +    $P -> Q$ is a \emph{program} that converts a proof (value) of $P$ into a
          162  +    proof (value) of $Q$!
          163  +\end{itemize}
          164  +
          165  +(End of aside.)
          166  +
          167  +\end{frame}
    68    168   
    69         -\subsection{Demostration}
          169  +
    70    170   
    71    171   
    72    172   \begin{frame}
    73    173   \vfill
    74    174   \centering
    75    175   A quick demo of a proof in Arend
    76    176   \vfill