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

Added presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

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