Check-in [8547fc1005]

Not logged in

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

Overview
Comment:Finished poster.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:8547fc10058af44f6796e292c113c6f141116b2d
User & Date: andy 2015-04-23 16:08:33
Context
2015-04-26
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
2015-04-22
20:50
Presentation work. check-in: 1275718981 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.

15
16
17
18
19
20
21


22
23
24
25
26
27
28
29
30
31
32


33
34
35
36
37
38
39
..
46
47
48
49
50
51
52

53
54
55
56
57
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
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224

















225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[landscape,a0paper,fontscale=0.285]{baposter} % Adjust the font scale/size here



\usepackage{graphicx} % Required for including images
\graphicspath{{figures/}} % Directory in which figures are stored

\usepackage{amsmath} % For typesetting math
\usepackage{amssymb} % Adds new symbols to be used in math mode

\usepackage{booktabs} % Top and bottom rules for tables
\usepackage{enumitem} % Used to reduce itemize/enumerate spacing
%\usepackage{palatino} % Use the Palatino font
\usepackage[font=small,labelfont=bf]{caption} % Required for specifying captions to tables and figures



% Setup fonts.
\usepackage{fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setmainfont[Numbers=OldStyle]{Junicode}
\setsansfont[Numbers=OldStyle,Scale=MatchLowercase]{Raleway}
\setmonofont[Scale=MatchLowercase]{Fantasque Sans Mono}
................................................................................

\usepackage{multicol} % Required for multiple columns
\setlength{\columnsep}{1.5em} % Slightly increase the space between columns
\setlength{\columnseprule}{0mm} % No horizontal rule between columns

\usepackage{tikz} % Required for flow chart
\usetikzlibrary{shapes,arrows} % Tikz libraries required for the flow chart in the template


\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}
{

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=black, % 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=white, % 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 
%----------------------------------------------------------------------------------------
%
{\includegraphics[height=4em]{logo.png}} % 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} California State University, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
{\includegraphics[height=4em]{logo.png}} % Second university/lab logo on the right

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

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

Donec non nisl a \textbf{arcu consequat} varius. Sed suscipit cursus luctus. Nulla sit amet elit augue. Curabitur scelerisque mollis dolor, quis blandit lorem condimentum at. Pellentesque sed nibh vel \textbf{dolor} sagittis semper. 

\begin{enumerate}\compresslist
\item Feugiat vitae elit
\item bibendum ante sed lacinia eros in
\item Curabitur scelerisque arcu consequat varius
\item Dapibus nulla id purus consectetur
\item Fringilla integer 
\end{enumerate}







\vspace{0.3em} % When there are two boxes, some whitespace may need to be added if the one on the right has more content
}

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

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

Aliquam non lacus dolor, \textit{a aliquam quam}. Cum sociis natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus. Nulla in nibh mauris. Donec vel ligula nisi, a lacinia arcu. Sed mi dui, malesuada vel consectetur et, egestas porta nisi. Sed eleifend pharetra dolor, et dapibus est vulputate eu. \textbf{Integer faucibus elementum felis vitae fringilla.} In hac habitasse platea dictumst. Duis tristique rutrum nisl, nec vulputate elit porta ut. Donec sodales sollicitudin turpis sed convallis. Etiam mauris ligula, blandit adipiscing condimentum eu, dapibus pellentesque risus.












}

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

\headerbox{Results 1}{name=results,column=2,span=2,row=0}{

\begin{multicols}{2}
\vspace{1em}

\begin{center}
\includegraphics[width=0.8\linewidth]{placeholder}
\captionof{figure}{Figure caption}
\end{center}

Aliquam auctor, metus id ultrices porta, risus enim cursus sapien, quis iaculis sapien tortor sed odio. Mauris ante orci, euismod vitae tincidunt eu, porta ut neque. Aenean sapien est, viverra vel lacinia nec, venenatis eu nulla. Maecenas ut nunc nibh, et tempus libero. Aenean vitae risus ante. Pellentesque condimentum dui. Etiam sagittis purus non tellus tempor volutpat. Donec et dui non massa tristique adipiscing.





\end{multicols}

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

\begin{multicols}{2}
\vspace{1em}
Sed fringilla tempus hendrerit. Vestibulum ante ipsum primis in faucibus orci luctus et ultrices posuere cubilia Curae; Etiam ut elit sit amet metus lobortis consequat sit amet in libero. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Phasellus vel sem magna. Nunc at convallis urna. isus ante. Pellentesque condimentum dui. Etiam sagittis purus non tellus tempor volutpat. Donec et dui non massa tristique adipiscing. Quisque vestibulum eros eu.

\begin{center}


\includegraphics[width=0.8\linewidth]{placeholder}













\captionof{figure}{Figure caption}
\end{center}

\end{multicols}
}

%----------------------------------------------------------------------------------------
%	REFERENCES
%----------------------------------------------------------------------------------------



\headerbox{References}{name=references,column=0,above=bottom}{

\renewcommand{\section}[2]{\vskip 0.05em} % Get rid of the default "References" section title
\nocite{*} % Insert publications even if they are not cited in the poster
\small{ % Reduce the font size in this block

\bibliographystyle{unsrt}
\bibliography{sample} % Use sample.bib as the bibliography file

}}

%----------------------------------------------------------------------------------------
%	FUTURE RESEARCH
%----------------------------------------------------------------------------------------

\headerbox{Future Research}{name=futureresearch,column=1,span=2,aligned=references,above=bottom}{ % This block is as tall as the references block


\begin{multicols}{2}
Integer sed lectus vel mauris euismod suscipit. Praesent a est a est ultricies pellentesque. Donec tincidunt, nunc in feugiat varius, lectus lectus auctor lorem, egestas molestie risus erat ut nibh.


Maecenas viverra ligula a risus blandit vel tincidunt est adipiscing. Suspendisse mollis iaculis sem, in \emph{imperdiet} orci porta vitae. Quisque id dui sed ante sollicitudin sagittis.







\end{multicols}
}

%----------------------------------------------------------------------------------------
%	CONTACT INFORMATION
%----------------------------------------------------------------------------------------

\headerbox{Contact Information}{name=contact,column=3,aligned=references,above=bottom}{ % This block is as tall as the references block

\begin{description}\compresslist
\item[Web] www.university.edu/smithlab
\item[Email] john@smith.com
\item[Phone] +1 (000) 111 1111
\end{description}
}

%----------------------------------------------------------------------------------------
%	CONCLUSION
%----------------------------------------------------------------------------------------

\headerbox{Conclusion}{name=conclusion,column=2,span=2,row=0,below=results,above=references}{

\begin{multicols}{2}

\tikzstyle{decision} = [diamond, draw, fill=blue!20, text width=4.5em, text badly centered, node distance=2cm, inner sep=0pt]
\tikzstyle{block} = [rectangle, draw, fill=blue!20, text width=5em, text centered, rounded corners, minimum height=4em]
\tikzstyle{line} = [draw, -latex']
\tikzstyle{cloud} = [draw, ellipse, fill=red!20, node distance=3cm, minimum height=2em]

\begin{tikzpicture}[node distance = 2cm, auto]
\node [block] (init) {Initialize Model};
\node [cloud, left of=init] (Start) {Start};
\node [cloud, right of=init] (Start2) {Start Two};
\node [block, below of=init] (init2) {Initialize Two};
\node [decision, below of=init2] (End) {End};
\path [line] (init) -- (init2);
\path [line] (init2) -- (End);
\path [line, dashed] (Start) -- (init);
\path [line, dashed] (Start2) -- (init);
\path [line, dashed] (Start2) |- (init2);
\end{tikzpicture}

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

\begin{itemize}\compresslist
\item Pellentesque eget orci eros. Fusce ultricies, tellus et pellentesque fringilla, ante massa luctus libero, quis tristique purus urna nec nibh. Phasellus fermentum rutrum elementum. Nam quis justo lectus.
\item Vestibulum sem ante, hendrerit a gravida ac, blandit quis magna.
\item Donec sem metus, facilisis at condimentum eget, vehicula ut massa. Morbi consequat, diam sed convallis tincidunt, arcu nunc.
\item Nunc at convallis urna. isus ante. Pellentesque condimentum dui. Etiam sagittis purus non tellus tempor volutpat. Donec et dui non massa tristique adipiscing.
\end{itemize}

\end{multicols}

















}

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

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

The following materials were required to complete the research:

\begin{itemize}\compresslist
\item Curabitur pellentesque dignissim
\item Eu facilisis est tempus quis
\item Duis porta consequat lorem
\item Eu facilisis est tempus quis
\end{itemize}

The following equations were used for statistical analysis:

\begin{equation}
\cos^3 \theta =\frac{1}{4}\cos\theta+\frac{3}{4}\cos 3\theta
\label{eq:refname}
\end{equation}\

\begin{equation}
E = mc^{2}
\label{eqn:Einstein}
\end{equation}

Phasellus imperdiet, tortor vitae congue bibendum, felis enim sagittis lorem, et volutpat ante orci sagittis mi. Morbi rutrum laoreet semper. Morbi accumsan enim nec tortor consectetur non commodo nisi sollicitudin. Proin sollicitudin. Pellentesque eget orci eros. Fusce ultricies, tellus et pellentesque fringilla, ante massa luctus libero, quis tristique purus urna nec nibh.
}

%----------------------------------------------------------------------------------------
%	RESULTS 2
%----------------------------------------------------------------------------------------

\headerbox{Results 2}{name=results2,column=1,below=objectives,bottomaligned=conclusion}{ % This block's bottom aligns with the bottom of the conclusion block

Donec faucibus purus at tortor egestas eu fermentum dolor facilisis. Maecenas tempor dui eu neque fringilla rutrum. Mauris \emph{lobortis} nisl accumsan.

\begin{center}
\begin{tabular}{l l l}
\toprule
\textbf{Treatments} & \textbf{Response 1} & \textbf{Response 2}\\
\midrule
Treatment 1 & 0.0003262 & 0.562 \\
Treatment 2 & 0.0015681 & 0.910 \\
Treatment 3 & 0.0009271 & 0.296 \\
\bottomrule
\end{tabular}
\captionof{table}{Table caption}
\end{center}

Nulla ut porttitor enim. Suspendisse venenatis dui eget eros gravida tempor. Mauris feugiat elit et augue placerat ultrices. Morbi accumsan enim nec tortor consectetur non commodo.

\begin{center}
\begin{tabular}{l l l}
\toprule
\textbf{Treatments} & \textbf{Response 1} & \textbf{Response 2}\\
\midrule
Treatment 1 & 0.0003262 & 0.562 \\
Treatment 2 & 0.0015681 & 0.910 \\
Treatment 3 & 0.0009271 & 0.296 \\
\bottomrule
\end{tabular}
\captionof{table}{Table caption}
\end{center}
}

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

\end{poster}

\end{document}







>
>











>
>







 







>













>





|

|













|

|
|





|
|
|
|
|
|
|
|
|
|
|
>
>
>
>
>
>










|
>
>
>
>
>
>
>
>
>
>
>
>






|


<
>
|
|
|
|

|
>
>
>
>
>




|
<
<


>
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
|


|






>
>
|
<

|

>
|
<
>







<
>

|
<
>
|
>
>
>
>
>
>
>










|
|
|







|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>






|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<






|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|







15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
..
50
51
52
53
54
55
56
57
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
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198

199
200
201
202
203

204
205
206
207
208
209
210
211

212
213
214

215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
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
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[landscape,a0paper,fontscale=0.285]{baposter} % Adjust the font scale/size here

\usepackage[inference]{semantic}

\usepackage{graphicx} % Required for including images
\graphicspath{{figures/}} % Directory in which figures are stored

\usepackage{amsmath} % For typesetting math
\usepackage{amssymb} % Adds new symbols to be used in math mode

\usepackage{booktabs} % Top and bottom rules for tables
\usepackage{enumitem} % Used to reduce itemize/enumerate spacing
%\usepackage{palatino} % Use the Palatino font
\usepackage[font=small,labelfont=bf]{caption} % Required for specifying captions to tables and figures

\usepackage{bibentry}

% Setup fonts.
\usepackage{fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setmainfont[Numbers=OldStyle]{Junicode}
\setsansfont[Numbers=OldStyle,Scale=MatchLowercase]{Raleway}
\setmonofont[Scale=MatchLowercase]{Fantasque Sans Mono}
................................................................................

\usepackage{multicol} % Required for multiple columns
\setlength{\columnsep}{1.5em} % Slightly increase the space between columns
\setlength{\columnseprule}{0mm} % No horizontal rule between columns

\usepackage{tikz} % Required for flow chart
\usetikzlibrary{shapes,arrows} % Tikz libraries required for the flow chart in the template
\usepackage{hf-tikz} % For highlighting math elements

\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:
\begin{itemize}\compresslist
\item Intuitionistic: proofs are evidential
\item Formal: first-order Horn clauses, explicit $\forall$ and $\exists$
\item Graphical: proofs as trees rather than text
\item Interactive: direct manipulation to construct proofs
\item Extensible: instructor-authored specifications 
\end{itemize}

\vspace{0.3em} % When there are two boxes, some whitespace may need to be added if the one on the right has more content
}

%----------------------------------------------------------------------------------------
%	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. 

Proof trees within the reasoning logic combine the inference rules from the
specification with those defining the reasoning logic.

\end{multicols}

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

%\begin{multicols}{2}



\begin{center}
\[
\inference*[]
    {\inference*[$X = z$]
        {\inference*[$Z = Y$]{}{\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Y)}}
        {\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Z)} &
     \inference*[$X = s(N)$]
        {\inference*[$Z = s(Z')$, IH]
            {}
            {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
         \mathsf{add}(N,Y,Z')}}
        {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
         \mathsf{add}(s(N),Y,Z)}
    }
    {\mathsf{nat}^\uparrow (X), \mathsf{nat}(Y) \vdash 
      \mathsf{add}(X,Y,Z)}
\]
\captionof{figure}{Proof of functionality of $\mathsf{add}$}
\end{center}

%\end{multicols}
}

%----------------------------------------------------------------------------------------
%	REFERENCES
%----------------------------------------------------------------------------------------

% You have to have some text in the references box, as the future research
% and contact information boxes have their height linked to it.
\headerbox{References}{name=references,column=0,span=1,above=bottom}{

\renewcommand{\section}[2]{\vskip 0.05em} % Get rid of the default "References" section title
%\nocite{*} % Insert publications even if they are not cited in the poster
\small{ % Reduce the font size in this block
\nobibliography{andy}
\bibliographystyle{abbrvnat}

\bibentry{clifton2015arend}
}}

%----------------------------------------------------------------------------------------
%	FUTURE RESEARCH
%----------------------------------------------------------------------------------------

\headerbox{Future Research}{name=futureresearch,column=1,span=2,aligned=references,above=bottom}{ % This block is as tall as the references block

\vspace{-0.5em}
\begin{multicols}{2}
\begin{itemize}\compresslist % Can't have more than six items

\item Formalization of specification and reasoning logics
\item Additional interactivity of complex specifications
\item Tactics for proof simplification
\end{itemize}
\begin{itemize}\compresslist
\item Ecosystem for large-scale use
\item Alternate proof presentations
\item Equational reasoning
\end{itemize}
\end{multicols}
}

%----------------------------------------------------------------------------------------
%	CONTACT INFORMATION
%----------------------------------------------------------------------------------------

\headerbox{Contact Information}{name=contact,column=3,aligned=references,above=bottom}{ % This block is as tall as the references block

\begin{description}\compresslist
\item[Web] http://fossil.twicetwo.com/arend.pl
\item[Email] andyclifton@mail.fresnostate.edu
\item[Phone] (559) 301-4442
\end{description}
}

%----------------------------------------------------------------------------------------
%	CONCLUSION
%----------------------------------------------------------------------------------------

\headerbox{User Interface}{name=conclusion,column=2,span=2,row=0,below=results}{

\begin{center}
\[
\inference[]
    {\inference[$X = z$]
        {?}
        {\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Z)} &
     \inference[$X = s(N)$]
        {?}
        {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
         \tikzmarkin{a}\mathsf{add}(s(N),Y,Z)\tikzmarkend{a}}
    }
    {\mathsf{nat}^\uparrow (X), \mathsf{nat}(Y) \vdash 
      \mathsf{add}(X,Y,Z)}
\]
\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}

}

%----------------------------------------------------------------------------------------
%	RESULTS 2
%----------------------------------------------------------------------------------------

\headerbox{Specification Logic}{name=results2,column=1,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block

\begin{center}
\[
\inference[Nat-Z]
    {}
    {\mathsf{nat}(z)}
\quad
\inference[Nat-S]
    {\mathsf{nat(X)}}
    {\mathsf{nat(s(X))}}
\]
\captionof{figure}{Inductive definition of $\mathbb{N}$}
\end{center}

The specification logic
is a first-order logic based on Horn clauses:
\[
U \leftarrow (P \land Q \land \ldots \land T)
\]
Graphically, this would be rendered as an inference rule:
\[
\inference[]
    {P & Q & \ldots & T}
    {U}
\]

Goals in the specification logic can be \emph{executed} according to the 
traditional resolution proof search procedure. Because our logic is constructive,
the result of a successful search is not just a substitution, but also a proof
tree.
}

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

\end{poster}

\end{document}