Index: poster/arend-poster.pdf
==================================================================
--- poster/arend-poster.pdf
+++ poster/arend-poster.pdf
cannot compute difference between binary files
Index: poster/arend-poster.tex
==================================================================
--- poster/arend-poster.tex
+++ poster/arend-poster.tex
@@ -60,11 +60,13 @@
\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}
{
@@ -74,36 +76,35 @@
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
+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
+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
+{\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}{
-\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.
@@ -124,22 +125,21 @@
% 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
+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 inductive proofs.
+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 never unaware of the (in)correctness of their proof. This eliminates
+student is always aware of the (in)correctness of their proof. This eliminates
the delay between construction and correction.
}
%----------------------------------------------------------------------------------------
% RESULTS 1
@@ -147,11 +147,10 @@
\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
@@ -262,11 +261,11 @@
\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,
@@ -277,16 +276,17 @@
\end{multicols}
}
\headerbox{Proof by Induction}{name=induction,column=2,span=2,row=0,below=auto,above=references}{
-\setlength{\parindent}{5ex}
+\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 subsumes natural number induction, strong induction, and structural
+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}
@@ -296,27 +296,27 @@
% 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
+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 spec. logic
+\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 a HTTP API for the above
+\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
- grammar file)
+ 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}
}