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

Changes to poster/arend-poster.pdf.

cannot compute difference between binary files

Changes to poster/arend-poster.tex.

    58     58   
    59     59   \newcommand{\compresslist}{ % Define a command to reduce spacing within itemize/enumerate environments, this is used right after \begin{itemize} or \begin{enumerate}
    60     60   \setlength{\itemsep}{1pt}
    61     61   \setlength{\parskip}{0pt}
    62     62   \setlength{\parsep}{0pt}
    63     63   }
    64     64   
           65  +\definecolor{trueblack}{rgb}{0,    0,     0}
    65     66   \definecolor{lightblue}{rgb}{0.145,0.6666,1} % Defines the color used for content box headers
           67  +
    66     68   
    67     69   \begin{document}
    68     70   
    69     71   \begin{poster}
    70     72   {
    71     73   %grid=true,
    72     74   headerborder=closed, % Adds a border around the header of content boxes
    73     75   colspacing=1em, % Column spacing
    74     76   bgColorOne=white, % Background color for the gradient on the left side of the poster
    75     77   bgColorTwo=white, % Background color for the gradient on the right side of the poster
    76     78   borderColor=lightblue, % Border color
    77     79   headerColorOne=lightblue, % Background color for the header in the content boxes (left side)
    78     80   headerColorTwo=lightblue, % Background color for the header in the content boxes (right side)
    79         -headerFontColor=black, % Text color for the header text in the content boxes
           81  +headerFontColor=trueblack, % Text color for the header text in the content boxes
    80     82   boxColorOne=white, % Background color of the content boxes
    81     83   textborder=roundedleft, % Format of the border around content boxes, can be: none, bars, coils, triangles, rectangle, rounded, roundedsmall, roundedright or faded
    82     84   eyecatcher=true, % Set to false for ignoring the left logo in the title and move the title left
    83     85   headerheight=0.1\textheight, % Height of the header
    84     86   headershape=roundedright, % Specify the rounded corner in the content box headers, can be: rectangle, small-rounded, roundedright, roundedleft or rounded
    85     87   headerfont=\Large\bf\textsc, % Large, bold and sans serif font in the headers of content boxes
    86         -%textfont={\setlength{\parindent}{1.5em}}, % Uncomment for paragraph indentation
           88  +textfont={\setlength{\parindent}{1.5em}}, % Uncomment for paragraph indentation
    87     89   linewidth=2pt % Width of the border lines around content boxes
    88     90   }
    89     91   %----------------------------------------------------------------------------------------
    90     92   %	TITLE SECTION 
    91     93   %----------------------------------------------------------------------------------------
    92     94   %
    93     95   {} % First university/lab logo on the left
    94         -{\bf\textsc{Arend --- Proof Assistant Assisted Pegagogy}\vspace{0.5em}} % Poster title
           96  +{\bf\textsc{Arend --- Proof Assistant Assisted Pedagogy}\vspace{0.5em}} % Poster title
    95     97   {\textsc{\{ Andrew V. Clifton \} \hspace{12pt} CSU, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
    96     98   {} % Second university/lab logo on the right
    97     99   
    98    100   %----------------------------------------------------------------------------------------
    99    101   %	OBJECTIVES
   100    102   %----------------------------------------------------------------------------------------
   101    103   
   102    104   \headerbox{Overview}{name=objectives,column=0,row=0}{
   103    105   
   104         -\setlength{\parindent}{5ex}
   105    106   Formal proof theory is integral to computer science education and practice.
   106    107   While tools for assisting in the development of formal proofs are common at the
   107    108   graduate and professional levels, their use in undergraduate curriculum has
   108    109   been surprisingly unexplored. We have developed \textsc{Arend}, a graphical,
   109    110   interactive proof assistant intended for use at the undergraduate level.
   110    111   
   111    112   Arend is:
................................................................................
   122    123   
   123    124   %----------------------------------------------------------------------------------------
   124    125   %	INTRODUCTION
   125    126   %----------------------------------------------------------------------------------------
   126    127   
   127    128   \headerbox{Introduction}{name=introduction,column=1,row=0,bottomaligned=objectives}{
   128    129   
   129         -\setlength{\parindent}{5ex}
   130    130   Arend implements proofs over an intuitionistic \emph{specification logic}, a
   131         -first-order logic based on Horn clauses. Proof are constructed in the
          131  +first-order logic based on Horn clauses. Proofs are constructed in a
   132    132   \emph{reasoning logic}, a superset of the specification logic with explicit
   133         -and implicit quantification, rightward implication, and inductive proofs.
          133  +and implicit quantification, rightward implication, and proof-by-induction.
   134    134   
   135    135   Visually, Arend presents proofs as \emph{derivations}, trees of rule-applications,
   136    136   where the rules are drawn from the specification. Specifications are also 
   137    137   presented graphically, as collections of inference rules.
   138    138   
   139    139   Because proofs in Arend are checked as they are constructed, interactively, the
   140         -student is never unaware of the (in)correctness of their proof. This eliminates
          140  +student is always aware of the (in)correctness of their proof. This eliminates
   141    141   the delay between construction and correction.
   142    142   }
   143    143   
   144    144   %----------------------------------------------------------------------------------------
   145    145   %	RESULTS 1
   146    146   %----------------------------------------------------------------------------------------
   147    147   
   148    148   \headerbox{Reasoning Logic}{name=results,column=2,span=2,row=0}{
   149    149   
   150    150   \begin{multicols}{2}
   151    151   
   152         -\setlength{\parindent}{5ex}
   153    152   Arend's reasoning logic is a first-order intuitionistic logic with implicit
   154    153   and explicit quantification ($\forall$ and $\exists$) and rightward implication.
   155    154   Negation is defined as refutation: $\neg P \equiv P \rightarrow \bot$.
   156    155   
   157    156   The specification logic can be embedded (syntactically and semantically) within
   158    157   the reasoning logic, allowing reasoning about specifications and goals. 
   159    158   
................................................................................
   260    259   \captionof{figure}{An incomplete proof tree}
   261    260   \end{center}
   262    261   
   263    262   \begin{multicols}{2}
   264    263   
   265    264   %------------------------------------------------
   266    265   
   267         -\setlength{\parindent}{5ex}
          266  +
   268    267   Figure~2 illustrates the proof tree in figure~1, during construction. Incomplete
   269    268   subproofs are indicated with $?$. The user has highlighted the consequent of the
   270    269   right subproof for interaction. \emph{Backchaining} the consequent will unify
   271    270   it against the rules for $\mathsf{add}$, replacing it with the premises of the
   272    271   matching rule. The elaboration procedure will only backchain to a single level,
   273    272   replacing $\mathsf{add}(s(N),Y,Z)$ with $\mathsf{add}(N,Y,Z_2)$ (together 
   274    273   with the substitution $Z = s(Z_2$). The less-incomplete proof is again presented
................................................................................
   275    274   to the user for further interaction.
   276    275   
   277    276   \end{multicols}
   278    277   }
   279    278   
   280    279   \headerbox{Proof by Induction}{name=induction,column=2,span=2,row=0,below=auto,above=references}{
   281    280   
   282         -\setlength{\parindent}{5ex}
          281  +\begin{multicols}{2}
   283    282   The target antecedent of an inductive proof is annotated $\uparrow$. 
   284    283   Case analysis of this goal will annotate any recursive calls with $\downarrow$.
   285    284   This indicates that the goal is now ``small'' enough for the IH to be applied.
   286         -This scheme subsumes natural number induction, strong induction, and structural
          285  +This scheme supports natural number induction, strong induction, and structural
   287    286   induction.
          287  +\end{multicols}
   288    288   \begin{center}
   289    289   $\mathsf{nat}^\downarrow(X) \land \mathsf{nat}(Y) \to \mathsf{add}(X,Y,Z)$
   290    290   \captionof{figure}{Inductive hypothesis of the proof in figure~1}
   291    291   \end{center}
   292    292   
   293    293   }
   294    294   
   295    295   %----------------------------------------------------------------------------------------
   296    296   %	MATERIALS AND METHODS
   297    297   %----------------------------------------------------------------------------------------
   298    298   
   299    299   \headerbox{Implementation}{name=method,column=0,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block
   300    300   
   301         -Arend's proof checking core is written in Prolog, while it's graphical front-end
          301  +Arend's proof checking core is written in Prolog, while its graphical front-end
   302    302   is web-based: JS, HTML, \& CSS. 
   303    303   
   304    304   Arend's backend:
   305    305   \begin{itemize}\compresslist
   306    306   \item Consists of \lnum{1,400} lines of Prolog in five modules
   307         -\item Implements execution and checking of proofs in the spec. logic
          307  +\item Implements execution and checking of proofs in the specification logic
   308    308   \item Implements checking of complete \& incomplete proofs in the reasoning logic
   309    309   \item Performs \emph{elaboration} of incomplete proofs: one-level replacement of
   310    310       ``holes'' in the proof tree with their valid subproof(s).
   311         -\item Provides a HTTP API for the above
          311  +\item Provides an HTTP API for the above
   312    312   \end{itemize}
   313    313   
   314    314   Arend's frontend:
   315    315   \begin{itemize}\compresslist
   316    316   \item Consists of \lnum{6,200} lines of Javascript (with a \lnum{700} line 
   317         -    grammar file)
          317  +    parser grammar file)
   318    318   \item Translates term objects to/from JS and Prolog
   319    319   \item Renders rule and proof objects as derivations
   320    320   \item Provides user interaction facilities
   321    321   \end{itemize}
   322    322   }
   323    323   
   324    324   %----------------------------------------------------------------------------------------