Check-in [b0f1fc67b4]

Not logged in

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

Overview
Comment:Fixed a typo in the poster.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:b0f1fc67b4a46cf0dc806f46a1e1c955aa493536
User & Date: andy 2015-04-26 16:26:09
Context
2015-04-26
16:27
Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk
16:26
Fixed a typo in the poster. check-in: b0f1fc67b4 user: andy tags: trunk
2015-04-23
16:08
Finished poster. check-in: 8547fc1005 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to poster/arend-poster.pdf.

cannot compute difference between binary files

Changes to poster/arend-poster.tex.

58
59
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
...
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
...
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
...
275
276
277
278
279
280
281
282
283
284
285
286
287

288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324

\newcommand{\compresslist}{ % Define a command to reduce spacing within itemize/enumerate environments, this is used right after \begin{itemize} or \begin{enumerate}
\setlength{\itemsep}{1pt}
\setlength{\parskip}{0pt}
\setlength{\parsep}{0pt}
}


\definecolor{lightblue}{rgb}{0.145,0.6666,1} % Defines the color used for content box headers


\begin{document}

\begin{poster}
{
%grid=true,
headerborder=closed, % Adds a border around the header of content boxes
colspacing=1em, % Column spacing
bgColorOne=white, % Background color for the gradient on the left side of the poster
bgColorTwo=white, % Background color for the gradient on the right side of the poster
borderColor=lightblue, % Border color
headerColorOne=lightblue, % Background color for the header in the content boxes (left side)
headerColorTwo=lightblue, % Background color for the header in the content boxes (right side)
headerFontColor=black, % Text color for the header text in the content boxes
boxColorOne=white, % Background color of the content boxes
textborder=roundedleft, % Format of the border around content boxes, can be: none, bars, coils, triangles, rectangle, rounded, roundedsmall, roundedright or faded
eyecatcher=true, % Set to false for ignoring the left logo in the title and move the title left
headerheight=0.1\textheight, % Height of the header
headershape=roundedright, % Specify the rounded corner in the content box headers, can be: rectangle, small-rounded, roundedright, roundedleft or rounded
headerfont=\Large\bf\textsc, % Large, bold and sans serif font in the headers of content boxes
%textfont={\setlength{\parindent}{1.5em}}, % Uncomment for paragraph indentation
linewidth=2pt % Width of the border lines around content boxes
}
%----------------------------------------------------------------------------------------
%	TITLE SECTION 
%----------------------------------------------------------------------------------------
%
{} % First university/lab logo on the left
{\bf\textsc{Arend --- Proof Assistant Assisted Pegagogy}\vspace{0.5em}} % Poster title
{\textsc{\{ Andrew V. Clifton \} \hspace{12pt} CSU, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
{} % Second university/lab logo on the right

%----------------------------------------------------------------------------------------
%	OBJECTIVES
%----------------------------------------------------------------------------------------

\headerbox{Overview}{name=objectives,column=0,row=0}{

\setlength{\parindent}{5ex}
Formal proof theory is integral to computer science education and practice.
While tools for assisting in the development of formal proofs are common at the
graduate and professional levels, their use in undergraduate curriculum has
been surprisingly unexplored. We have developed \textsc{Arend}, a graphical,
interactive proof assistant intended for use at the undergraduate level.

Arend is:
................................................................................

%----------------------------------------------------------------------------------------
%	INTRODUCTION
%----------------------------------------------------------------------------------------

\headerbox{Introduction}{name=introduction,column=1,row=0,bottomaligned=objectives}{

\setlength{\parindent}{5ex}
Arend implements proofs over an intuitionistic \emph{specification logic}, a
first-order logic based on Horn clauses. Proof are constructed in the
\emph{reasoning logic}, a superset of the specification logic with explicit
and implicit quantification, rightward implication, and inductive proofs.

Visually, Arend presents proofs as \emph{derivations}, trees of rule-applications,
where the rules are drawn from the specification. Specifications are also 
presented graphically, as collections of inference rules.

Because proofs in Arend are checked as they are constructed, interactively, the
student is never unaware of the (in)correctness of their proof. This eliminates
the delay between construction and correction.
}

%----------------------------------------------------------------------------------------
%	RESULTS 1
%----------------------------------------------------------------------------------------

\headerbox{Reasoning Logic}{name=results,column=2,span=2,row=0}{

\begin{multicols}{2}

\setlength{\parindent}{5ex}
Arend's reasoning logic is a first-order intuitionistic logic with implicit
and explicit quantification ($\forall$ and $\exists$) and rightward implication.
Negation is defined as refutation: $\neg P \equiv P \rightarrow \bot$.

The specification logic can be embedded (syntactically and semantically) within
the reasoning logic, allowing reasoning about specifications and goals. 

................................................................................
\captionof{figure}{An incomplete proof tree}
\end{center}

\begin{multicols}{2}

%------------------------------------------------

\setlength{\parindent}{5ex}
Figure~2 illustrates the proof tree in figure~1, during construction. Incomplete
subproofs are indicated with $?$. The user has highlighted the consequent of the
right subproof for interaction. \emph{Backchaining} the consequent will unify
it against the rules for $\mathsf{add}$, replacing it with the premises of the
matching rule. The elaboration procedure will only backchain to a single level,
replacing $\mathsf{add}(s(N),Y,Z)$ with $\mathsf{add}(N,Y,Z_2)$ (together 
with the substitution $Z = s(Z_2$). The less-incomplete proof is again presented
................................................................................
to the user for further interaction.

\end{multicols}
}

\headerbox{Proof by Induction}{name=induction,column=2,span=2,row=0,below=auto,above=references}{

\setlength{\parindent}{5ex}
The target antecedent of an inductive proof is annotated $\uparrow$. 
Case analysis of this goal will annotate any recursive calls with $\downarrow$.
This indicates that the goal is now ``small'' enough for the IH to be applied.
This scheme subsumes natural number induction, strong induction, and structural
induction.

\begin{center}
$\mathsf{nat}^\downarrow(X) \land \mathsf{nat}(Y) \to \mathsf{add}(X,Y,Z)$
\captionof{figure}{Inductive hypothesis of the proof in figure~1}
\end{center}

}

%----------------------------------------------------------------------------------------
%	MATERIALS AND METHODS
%----------------------------------------------------------------------------------------

\headerbox{Implementation}{name=method,column=0,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block

Arend's proof checking core is written in Prolog, while it's graphical front-end
is web-based: JS, HTML, \& CSS. 

Arend's backend:
\begin{itemize}\compresslist
\item Consists of \lnum{1,400} lines of Prolog in five modules
\item Implements execution and checking of proofs in the spec. logic
\item Implements checking of complete \& incomplete proofs in the reasoning logic
\item Performs \emph{elaboration} of incomplete proofs: one-level replacement of
    ``holes'' in the proof tree with their valid subproof(s).
\item Provides a HTTP API for the above
\end{itemize}

Arend's frontend:
\begin{itemize}\compresslist
\item Consists of \lnum{6,200} lines of Javascript (with a \lnum{700} line 
    grammar file)
\item Translates term objects to/from JS and Prolog
\item Renders rule and proof objects as derivations
\item Provides user interaction facilities
\end{itemize}
}

%----------------------------------------------------------------------------------------







>

>













|






|







|









<







 







<

|

|






|











<







 







|







 







|



|

>













|





|



|





|







58
59
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
...
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
...
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
...
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324

\newcommand{\compresslist}{ % Define a command to reduce spacing within itemize/enumerate environments, this is used right after \begin{itemize} or \begin{enumerate}
\setlength{\itemsep}{1pt}
\setlength{\parskip}{0pt}
\setlength{\parsep}{0pt}
}

\definecolor{trueblack}{rgb}{0,    0,     0}
\definecolor{lightblue}{rgb}{0.145,0.6666,1} % Defines the color used for content box headers


\begin{document}

\begin{poster}
{
%grid=true,
headerborder=closed, % Adds a border around the header of content boxes
colspacing=1em, % Column spacing
bgColorOne=white, % Background color for the gradient on the left side of the poster
bgColorTwo=white, % Background color for the gradient on the right side of the poster
borderColor=lightblue, % Border color
headerColorOne=lightblue, % Background color for the header in the content boxes (left side)
headerColorTwo=lightblue, % Background color for the header in the content boxes (right side)
headerFontColor=trueblack, % Text color for the header text in the content boxes
boxColorOne=white, % Background color of the content boxes
textborder=roundedleft, % Format of the border around content boxes, can be: none, bars, coils, triangles, rectangle, rounded, roundedsmall, roundedright or faded
eyecatcher=true, % Set to false for ignoring the left logo in the title and move the title left
headerheight=0.1\textheight, % Height of the header
headershape=roundedright, % Specify the rounded corner in the content box headers, can be: rectangle, small-rounded, roundedright, roundedleft or rounded
headerfont=\Large\bf\textsc, % Large, bold and sans serif font in the headers of content boxes
textfont={\setlength{\parindent}{1.5em}}, % Uncomment for paragraph indentation
linewidth=2pt % Width of the border lines around content boxes
}
%----------------------------------------------------------------------------------------
%	TITLE SECTION 
%----------------------------------------------------------------------------------------
%
{} % First university/lab logo on the left
{\bf\textsc{Arend --- Proof Assistant Assisted Pedagogy}\vspace{0.5em}} % Poster title
{\textsc{\{ Andrew V. Clifton \} \hspace{12pt} CSU, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
{} % Second university/lab logo on the right

%----------------------------------------------------------------------------------------
%	OBJECTIVES
%----------------------------------------------------------------------------------------

\headerbox{Overview}{name=objectives,column=0,row=0}{


Formal proof theory is integral to computer science education and practice.
While tools for assisting in the development of formal proofs are common at the
graduate and professional levels, their use in undergraduate curriculum has
been surprisingly unexplored. We have developed \textsc{Arend}, a graphical,
interactive proof assistant intended for use at the undergraduate level.

Arend is:
................................................................................

%----------------------------------------------------------------------------------------
%	INTRODUCTION
%----------------------------------------------------------------------------------------

\headerbox{Introduction}{name=introduction,column=1,row=0,bottomaligned=objectives}{


Arend implements proofs over an intuitionistic \emph{specification logic}, a
first-order logic based on Horn clauses. Proofs are constructed in a
\emph{reasoning logic}, a superset of the specification logic with explicit
and implicit quantification, rightward implication, and proof-by-induction.

Visually, Arend presents proofs as \emph{derivations}, trees of rule-applications,
where the rules are drawn from the specification. Specifications are also 
presented graphically, as collections of inference rules.

Because proofs in Arend are checked as they are constructed, interactively, the
student is always aware of the (in)correctness of their proof. This eliminates
the delay between construction and correction.
}

%----------------------------------------------------------------------------------------
%	RESULTS 1
%----------------------------------------------------------------------------------------

\headerbox{Reasoning Logic}{name=results,column=2,span=2,row=0}{

\begin{multicols}{2}


Arend's reasoning logic is a first-order intuitionistic logic with implicit
and explicit quantification ($\forall$ and $\exists$) and rightward implication.
Negation is defined as refutation: $\neg P \equiv P \rightarrow \bot$.

The specification logic can be embedded (syntactically and semantically) within
the reasoning logic, allowing reasoning about specifications and goals. 

................................................................................
\captionof{figure}{An incomplete proof tree}
\end{center}

\begin{multicols}{2}

%------------------------------------------------


Figure~2 illustrates the proof tree in figure~1, during construction. Incomplete
subproofs are indicated with $?$. The user has highlighted the consequent of the
right subproof for interaction. \emph{Backchaining} the consequent will unify
it against the rules for $\mathsf{add}$, replacing it with the premises of the
matching rule. The elaboration procedure will only backchain to a single level,
replacing $\mathsf{add}(s(N),Y,Z)$ with $\mathsf{add}(N,Y,Z_2)$ (together 
with the substitution $Z = s(Z_2$). The less-incomplete proof is again presented
................................................................................
to the user for further interaction.

\end{multicols}
}

\headerbox{Proof by Induction}{name=induction,column=2,span=2,row=0,below=auto,above=references}{

\begin{multicols}{2}
The target antecedent of an inductive proof is annotated $\uparrow$. 
Case analysis of this goal will annotate any recursive calls with $\downarrow$.
This indicates that the goal is now ``small'' enough for the IH to be applied.
This scheme supports natural number induction, strong induction, and structural
induction.
\end{multicols}
\begin{center}
$\mathsf{nat}^\downarrow(X) \land \mathsf{nat}(Y) \to \mathsf{add}(X,Y,Z)$
\captionof{figure}{Inductive hypothesis of the proof in figure~1}
\end{center}

}

%----------------------------------------------------------------------------------------
%	MATERIALS AND METHODS
%----------------------------------------------------------------------------------------

\headerbox{Implementation}{name=method,column=0,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block

Arend's proof checking core is written in Prolog, while its graphical front-end
is web-based: JS, HTML, \& CSS. 

Arend's backend:
\begin{itemize}\compresslist
\item Consists of \lnum{1,400} lines of Prolog in five modules
\item Implements execution and checking of proofs in the specification logic
\item Implements checking of complete \& incomplete proofs in the reasoning logic
\item Performs \emph{elaboration} of incomplete proofs: one-level replacement of
    ``holes'' in the proof tree with their valid subproof(s).
\item Provides an HTTP API for the above
\end{itemize}

Arend's frontend:
\begin{itemize}\compresslist
\item Consists of \lnum{6,200} lines of Javascript (with a \lnum{700} line 
    parser grammar file)
\item Translates term objects to/from JS and Prolog
\item Renders rule and proof objects as derivations
\item Provides user interaction facilities
\end{itemize}
}

%----------------------------------------------------------------------------------------