Check-in [a24ff57f47]

Not logged in

Overview
Comment: Presentation work. Added PDF of presentation. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders a24ff57f473fea7c6319fce2d16f15b424a0bf4c 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

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