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

    15     15   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    16     16   
    17     17   %----------------------------------------------------------------------------------------
    18     18   %	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
    19     19   %----------------------------------------------------------------------------------------
    20     20   
    21     21   \documentclass[landscape,a0paper,fontscale=0.285]{baposter} % Adjust the font scale/size here
           22  +
           23  +\usepackage[inference]{semantic}
    22     24   
    23     25   \usepackage{graphicx} % Required for including images
    24     26   \graphicspath{{figures/}} % Directory in which figures are stored
    25     27   
    26     28   \usepackage{amsmath} % For typesetting math
    27     29   \usepackage{amssymb} % Adds new symbols to be used in math mode
    28     30   
    29     31   \usepackage{booktabs} % Top and bottom rules for tables
    30     32   \usepackage{enumitem} % Used to reduce itemize/enumerate spacing
    31     33   %\usepackage{palatino} % Use the Palatino font
    32     34   \usepackage[font=small,labelfont=bf]{caption} % Required for specifying captions to tables and figures
           35  +
           36  +\usepackage{bibentry}
    33     37   
    34     38   % Setup fonts.
    35     39   \usepackage{fontspec}
    36     40   \defaultfontfeatures{Mapping=tex-text}
    37     41   \setmainfont[Numbers=OldStyle]{Junicode}
    38     42   \setsansfont[Numbers=OldStyle,Scale=MatchLowercase]{Raleway}
    39     43   \setmonofont[Scale=MatchLowercase]{Fantasque Sans Mono}
................................................................................
    46     50   
    47     51   \usepackage{multicol} % Required for multiple columns
    48     52   \setlength{\columnsep}{1.5em} % Slightly increase the space between columns
    49     53   \setlength{\columnseprule}{0mm} % No horizontal rule between columns
    50     54   
    51     55   \usepackage{tikz} % Required for flow chart
    52     56   \usetikzlibrary{shapes,arrows} % Tikz libraries required for the flow chart in the template
           57  +\usepackage{hf-tikz} % For highlighting math elements
    53     58   
    54     59   \newcommand{\compresslist}{ % Define a command to reduce spacing within itemize/enumerate environments, this is used right after \begin{itemize} or \begin{enumerate}
    55     60   \setlength{\itemsep}{1pt}
    56     61   \setlength{\parskip}{0pt}
    57     62   \setlength{\parsep}{0pt}
    58     63   }
    59     64   
    60     65   \definecolor{lightblue}{rgb}{0.145,0.6666,1} % Defines the color used for content box headers
    61     66   
    62     67   \begin{document}
    63     68   
    64     69   \begin{poster}
    65     70   {
           71  +%grid=true,
    66     72   headerborder=closed, % Adds a border around the header of content boxes
    67     73   colspacing=1em, % Column spacing
    68     74   bgColorOne=white, % Background color for the gradient on the left side of the poster
    69     75   bgColorTwo=white, % Background color for the gradient on the right side of the poster
    70     76   borderColor=lightblue, % Border color
    71         -headerColorOne=black, % Background color for the header in the content boxes (left side)
           77  +headerColorOne=lightblue, % Background color for the header in the content boxes (left side)
    72     78   headerColorTwo=lightblue, % Background color for the header in the content boxes (right side)
    73         -headerFontColor=white, % Text color for the header text in the content boxes
           79  +headerFontColor=black, % Text color for the header text in the content boxes
    74     80   boxColorOne=white, % Background color of the content boxes
    75     81   textborder=roundedleft, % Format of the border around content boxes, can be: none, bars, coils, triangles, rectangle, rounded, roundedsmall, roundedright or faded
    76     82   eyecatcher=true, % Set to false for ignoring the left logo in the title and move the title left
    77     83   headerheight=0.1\textheight, % Height of the header
    78     84   headershape=roundedright, % Specify the rounded corner in the content box headers, can be: rectangle, small-rounded, roundedright, roundedleft or rounded
    79     85   headerfont=\Large\bf\textsc, % Large, bold and sans serif font in the headers of content boxes
    80     86   %textfont={\setlength{\parindent}{1.5em}}, % Uncomment for paragraph indentation
    81     87   linewidth=2pt % Width of the border lines around content boxes
    82     88   }
    83     89   %----------------------------------------------------------------------------------------
    84     90   %	TITLE SECTION 
    85     91   %----------------------------------------------------------------------------------------
    86     92   %
    87         -{\includegraphics[height=4em]{logo.png}} % First university/lab logo on the left
           93  +{} % First university/lab logo on the left
    88     94   {\bf\textsc{Arend --- Proof Assistant Assisted Pegagogy}\vspace{0.5em}} % Poster title
    89         -{\textsc{\{ Andrew V. Clifton \} \hspace{12pt} California State University, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
    90         -{\includegraphics[height=4em]{logo.png}} % Second university/lab logo on the right
           95  +{\textsc{\{ Andrew V. Clifton \} \hspace{12pt} CSU, Fresno; College of Science and Mathematics; Computer Science Dept.}} % Author names and institution
           96  +{} % Second university/lab logo on the right
    91     97   
    92     98   %----------------------------------------------------------------------------------------
    93     99   %	OBJECTIVES
    94    100   %----------------------------------------------------------------------------------------
    95    101   
    96         -\headerbox{Objectives}{name=objectives,column=0,row=0}{
          102  +\headerbox{Overview}{name=objectives,column=0,row=0}{
    97    103   
    98         -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. 
          104  +\setlength{\parindent}{5ex}
          105  +Formal proof theory is integral to computer science education and practice.
          106  +While tools for assisting in the development of formal proofs are common at the
          107  +graduate and professional levels, their use in undergraduate curriculum has
          108  +been surprisingly unexplored. We have developed \textsc{Arend}, a graphical,
          109  +interactive proof assistant intended for use at the undergraduate level.
    99    110   
   100         -\begin{enumerate}\compresslist
   101         -\item Feugiat vitae elit
   102         -\item bibendum ante sed lacinia eros in
   103         -\item Curabitur scelerisque arcu consequat varius
   104         -\item Dapibus nulla id purus consectetur
   105         -\item Fringilla integer 
   106         -\end{enumerate}
          111  +Arend is:
          112  +\begin{itemize}\compresslist
          113  +\item Intuitionistic: proofs are evidential
          114  +\item Formal: first-order Horn clauses, explicit $\forall$ and $\exists$
          115  +\item Graphical: proofs as trees rather than text
          116  +\item Interactive: direct manipulation to construct proofs
          117  +\item Extensible: instructor-authored specifications 
          118  +\end{itemize}
   107    119   
   108    120   \vspace{0.3em} % When there are two boxes, some whitespace may need to be added if the one on the right has more content
   109    121   }
   110    122   
   111    123   %----------------------------------------------------------------------------------------
   112    124   %	INTRODUCTION
   113    125   %----------------------------------------------------------------------------------------
   114    126   
   115    127   \headerbox{Introduction}{name=introduction,column=1,row=0,bottomaligned=objectives}{
   116    128   
   117         -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.
          129  +\setlength{\parindent}{5ex}
          130  +Arend implements proofs over an intuitionistic \emph{specification logic}, a
          131  +first-order logic based on Horn clauses. Proof are constructed in the
          132  +\emph{reasoning logic}, a superset of the specification logic with explicit
          133  +and implicit quantification, rightward implication, and inductive proofs.
          134  +
          135  +Visually, Arend presents proofs as \emph{derivations}, trees of rule-applications,
          136  +where the rules are drawn from the specification. Specifications are also 
          137  +presented graphically, as collections of inference rules.
          138  +
          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
          141  +the delay between construction and correction.
   118    142   }
   119    143   
   120    144   %----------------------------------------------------------------------------------------
   121    145   %	RESULTS 1
   122    146   %----------------------------------------------------------------------------------------
   123    147   
   124         -\headerbox{Results 1}{name=results,column=2,span=2,row=0}{
          148  +\headerbox{Reasoning Logic}{name=results,column=2,span=2,row=0}{
   125    149   
   126    150   \begin{multicols}{2}
   127         -\vspace{1em}
   128         -\begin{center}
   129         -\includegraphics[width=0.8\linewidth]{placeholder}
   130         -\captionof{figure}{Figure caption}
   131         -\end{center}
   132    151   
   133         -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.
          152  +\setlength{\parindent}{5ex}
          153  +Arend's reasoning logic is a first-order intuitionistic logic with implicit
          154  +and explicit quantification ($\forall$ and $\exists$) and rightward implication.
          155  +Negation is defined as refutation: $\neg P \equiv P \rightarrow \bot$.
          156  +
          157  +The specification logic can be embedded (syntactically and semantically) within
          158  +the reasoning logic, allowing reasoning about specifications and goals. 
          159  +
          160  +Proof trees within the reasoning logic combine the inference rules from the
          161  +specification with those defining the reasoning logic.
          162  +
   134    163   \end{multicols}
   135    164   
   136    165   %------------------------------------------------
   137    166   
   138         -\begin{multicols}{2}
   139         -\vspace{1em}
   140         -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.
          167  +%\begin{multicols}{2}
   141    168   
   142    169   \begin{center}
   143         -\includegraphics[width=0.8\linewidth]{placeholder}
   144         -\captionof{figure}{Figure caption}
          170  +\[
          171  +\inference*[]
          172  +    {\inference*[$X = z$]
          173  +        {\inference*[$Z = Y$]{}{\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Y)}}
          174  +        {\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Z)} &
          175  +     \inference*[$X = s(N)$]
          176  +        {\inference*[$Z = s(Z')$, IH]
          177  +            {}
          178  +            {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
          179  +         \mathsf{add}(N,Y,Z')}}
          180  +        {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
          181  +         \mathsf{add}(s(N),Y,Z)}
          182  +    }
          183  +    {\mathsf{nat}^\uparrow (X), \mathsf{nat}(Y) \vdash 
          184  +      \mathsf{add}(X,Y,Z)}
          185  +\]
          186  +\captionof{figure}{Proof of functionality of $\mathsf{add}$}
   145    187   \end{center}
   146    188   
   147         -\end{multicols}
          189  +%\end{multicols}
   148    190   }
   149    191   
   150    192   %----------------------------------------------------------------------------------------
   151    193   %	REFERENCES
   152    194   %----------------------------------------------------------------------------------------
   153    195   
   154         -\headerbox{References}{name=references,column=0,above=bottom}{
   155         -
          196  +% You have to have some text in the references box, as the future research
          197  +% and contact information boxes have their height linked to it.
          198  +\headerbox{References}{name=references,column=0,span=1,above=bottom}{
   156    199   \renewcommand{\section}[2]{\vskip 0.05em} % Get rid of the default "References" section title
   157         -\nocite{*} % Insert publications even if they are not cited in the poster
          200  +%\nocite{*} % Insert publications even if they are not cited in the poster
   158    201   \small{ % Reduce the font size in this block
   159         -\bibliographystyle{unsrt}
   160         -\bibliography{sample} % Use sample.bib as the bibliography file
          202  +\nobibliography{andy}
          203  +\bibliographystyle{abbrvnat}
          204  +\bibentry{clifton2015arend}
   161    205   }}
   162    206   
   163    207   %----------------------------------------------------------------------------------------
   164    208   %	FUTURE RESEARCH
   165    209   %----------------------------------------------------------------------------------------
   166    210   
   167    211   \headerbox{Future Research}{name=futureresearch,column=1,span=2,aligned=references,above=bottom}{ % This block is as tall as the references block
   168         -
          212  +\vspace{-0.5em}
   169    213   \begin{multicols}{2}
   170         -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.
   171         -
   172         -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.
          214  +\begin{itemize}\compresslist % Can't have more than six items
          215  +\item Formalization of specification and reasoning logics
          216  +\item Additional interactivity of complex specifications
          217  +\item Tactics for proof simplification
          218  +\end{itemize}
          219  +\begin{itemize}\compresslist
          220  +\item Ecosystem for large-scale use
          221  +\item Alternate proof presentations
          222  +\item Equational reasoning
          223  +\end{itemize}
   173    224   \end{multicols}
   174    225   }
   175    226   
   176    227   %----------------------------------------------------------------------------------------
   177    228   %	CONTACT INFORMATION
   178    229   %----------------------------------------------------------------------------------------
   179    230   
   180    231   \headerbox{Contact Information}{name=contact,column=3,aligned=references,above=bottom}{ % This block is as tall as the references block
   181    232   
   182    233   \begin{description}\compresslist
   183         -\item[Web] www.university.edu/smithlab
   184         -\item[Email] john@smith.com
   185         -\item[Phone] +1 (000) 111 1111
          234  +\item[Web] http://fossil.twicetwo.com/arend.pl
          235  +\item[Email] andyclifton@mail.fresnostate.edu
          236  +\item[Phone] (559) 301-4442
   186    237   \end{description}
   187    238   }
   188    239   
   189    240   %----------------------------------------------------------------------------------------
   190    241   %	CONCLUSION
   191    242   %----------------------------------------------------------------------------------------
   192    243   
   193         -\headerbox{Conclusion}{name=conclusion,column=2,span=2,row=0,below=results,above=references}{
   194         -
   195         -\begin{multicols}{2}
   196         -
   197         -\tikzstyle{decision} = [diamond, draw, fill=blue!20, text width=4.5em, text badly centered, node distance=2cm, inner sep=0pt]
   198         -\tikzstyle{block} = [rectangle, draw, fill=blue!20, text width=5em, text centered, rounded corners, minimum height=4em]
   199         -\tikzstyle{line} = [draw, -latex']
   200         -\tikzstyle{cloud} = [draw, ellipse, fill=red!20, node distance=3cm, minimum height=2em]
   201         -
   202         -\begin{tikzpicture}[node distance = 2cm, auto]
   203         -\node [block] (init) {Initialize Model};
   204         -\node [cloud, left of=init] (Start) {Start};
   205         -\node [cloud, right of=init] (Start2) {Start Two};
   206         -\node [block, below of=init] (init2) {Initialize Two};
   207         -\node [decision, below of=init2] (End) {End};
   208         -\path [line] (init) -- (init2);
   209         -\path [line] (init2) -- (End);
   210         -\path [line, dashed] (Start) -- (init);
   211         -\path [line, dashed] (Start2) -- (init);
   212         -\path [line, dashed] (Start2) |- (init2);
   213         -\end{tikzpicture}
          244  +\headerbox{User Interface}{name=conclusion,column=2,span=2,row=0,below=results}{
          245  +
          246  +\begin{center}
          247  +\[
          248  +\inference[]
          249  +    {\inference[$X = z$]
          250  +        {?}
          251  +        {\mathsf{nat}(Y) \vdash \mathsf{add}(z,Y,Z)} &
          252  +     \inference[$X = s(N)$]
          253  +        {?}
          254  +        {\mathsf{nat}^\downarrow (N), \mathsf{nat}(Y) \vdash 
          255  +         \tikzmarkin{a}\mathsf{add}(s(N),Y,Z)\tikzmarkend{a}}
          256  +    }
          257  +    {\mathsf{nat}^\uparrow (X), \mathsf{nat}(Y) \vdash 
          258  +      \mathsf{add}(X,Y,Z)}
          259  +\]
          260  +\captionof{figure}{An incomplete proof tree}
          261  +\end{center}
          262  +
          263  +\begin{multicols}{2}
   214    264   
   215    265   %------------------------------------------------
   216    266   
   217         -\begin{itemize}\compresslist
   218         -\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.
   219         -\item Vestibulum sem ante, hendrerit a gravida ac, blandit quis magna.
   220         -\item Donec sem metus, facilisis at condimentum eget, vehicula ut massa. Morbi consequat, diam sed convallis tincidunt, arcu nunc.
   221         -\item Nunc at convallis urna. isus ante. Pellentesque condimentum dui. Etiam sagittis purus non tellus tempor volutpat. Donec et dui non massa tristique adipiscing.
   222         -\end{itemize}
          267  +\setlength{\parindent}{5ex}
          268  +Figure~2 illustrates the proof tree in figure~1, during construction. Incomplete
          269  +subproofs are indicated with $?$. The user has highlighted the consequent of the
          270  +right subproof for interaction. \emph{Backchaining} the consequent will unify
          271  +it against the rules for $\mathsf{add}$, replacing it with the premises of the
          272  +matching rule. The elaboration procedure will only backchain to a single level,
          273  +replacing $\mathsf{add}(s(N),Y,Z)$ with $\mathsf{add}(N,Y,Z_2)$ (together 
          274  +with the substitution $Z = s(Z_2$). The less-incomplete proof is again presented
          275  +to the user for further interaction.
   223    276   
   224    277   \end{multicols}
          278  +}
          279  +
          280  +\headerbox{Proof by Induction}{name=induction,column=2,span=2,row=0,below=auto,above=references}{
          281  +
          282  +\setlength{\parindent}{5ex}
          283  +The target antecedent of an inductive proof is annotated $\uparrow$. 
          284  +Case analysis of this goal will annotate any recursive calls with $\downarrow$.
          285  +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
          287  +induction.
          288  +\begin{center}
          289  +$\mathsf{nat}^\downarrow(X) \land \mathsf{nat}(Y) \to \mathsf{add}(X,Y,Z)$
          290  +\captionof{figure}{Inductive hypothesis of the proof in figure~1}
          291  +\end{center}
          292  +
   225    293   }
   226    294   
   227    295   %----------------------------------------------------------------------------------------
   228    296   %	MATERIALS AND METHODS
   229    297   %----------------------------------------------------------------------------------------
   230    298   
   231         -\headerbox{Materials \& Methods}{name=method,column=0,below=objectives,bottomaligned=conclusion}{ % This block's bottom aligns with the bottom of the conclusion block
          299  +\headerbox{Implementation}{name=method,column=0,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block
   232    300   
   233         -The following materials were required to complete the research:
          301  +Arend's proof checking core is written in Prolog, while it's graphical front-end
          302  +is web-based: JS, HTML, \& CSS. 
   234    303   
          304  +Arend's backend:
   235    305   \begin{itemize}\compresslist
   236         -\item Curabitur pellentesque dignissim
   237         -\item Eu facilisis est tempus quis
   238         -\item Duis porta consequat lorem
   239         -\item Eu facilisis est tempus quis
          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
          308  +\item Implements checking of complete \& incomplete proofs in the reasoning logic
          309  +\item Performs \emph{elaboration} of incomplete proofs: one-level replacement of
          310  +    ``holes'' in the proof tree with their valid subproof(s).
          311  +\item Provides a HTTP API for the above
   240    312   \end{itemize}
   241    313   
   242         -The following equations were used for statistical analysis:
   243         -
   244         -\begin{equation}
   245         -\cos^3 \theta =\frac{1}{4}\cos\theta+\frac{3}{4}\cos 3\theta
   246         -\label{eq:refname}
   247         -\end{equation}\
   248         -
   249         -\begin{equation}
   250         -E = mc^{2}
   251         -\label{eqn:Einstein}
   252         -\end{equation}
   253         -
   254         -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.
          314  +Arend's frontend:
          315  +\begin{itemize}\compresslist
          316  +\item Consists of \lnum{6,200} lines of Javascript (with a \lnum{700} line 
          317  +    grammar file)
          318  +\item Translates term objects to/from JS and Prolog
          319  +\item Renders rule and proof objects as derivations
          320  +\item Provides user interaction facilities
          321  +\end{itemize}
   255    322   }
   256    323   
   257    324   %----------------------------------------------------------------------------------------
   258    325   %	RESULTS 2
   259    326   %----------------------------------------------------------------------------------------
   260    327   
   261         -\headerbox{Results 2}{name=results2,column=1,below=objectives,bottomaligned=conclusion}{ % This block's bottom aligns with the bottom of the conclusion block
   262         -
   263         -Donec faucibus purus at tortor egestas eu fermentum dolor facilisis. Maecenas tempor dui eu neque fringilla rutrum. Mauris \emph{lobortis} nisl accumsan.
          328  +\headerbox{Specification Logic}{name=results2,column=1,below=objectives,bottomaligned=induction}{ % This block's bottom aligns with the bottom of the conclusion block
   264    329   
   265    330   \begin{center}
   266         -\begin{tabular}{l l l}
   267         -\toprule
   268         -\textbf{Treatments} & \textbf{Response 1} & \textbf{Response 2}\\
   269         -\midrule
   270         -Treatment 1 & 0.0003262 & 0.562 \\
   271         -Treatment 2 & 0.0015681 & 0.910 \\
   272         -Treatment 3 & 0.0009271 & 0.296 \\
   273         -\bottomrule
   274         -\end{tabular}
   275         -\captionof{table}{Table caption}
          331  +\[
          332  +\inference[Nat-Z]
          333  +    {}
          334  +    {\mathsf{nat}(z)}
          335  +\quad
          336  +\inference[Nat-S]
          337  +    {\mathsf{nat(X)}}
          338  +    {\mathsf{nat(s(X))}}
          339  +\]
          340  +\captionof{figure}{Inductive definition of $\mathbb{N}$}
   276    341   \end{center}
   277    342   
   278         -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.
          343  +The specification logic
          344  +is a first-order logic based on Horn clauses:
          345  +\[
          346  +U \leftarrow (P \land Q \land \ldots \land T)
          347  +\]
          348  +Graphically, this would be rendered as an inference rule:
          349  +\[
          350  +\inference[]
          351  +    {P & Q & \ldots & T}
          352  +    {U}
          353  +\]
   279    354   
   280         -\begin{center}
   281         -\begin{tabular}{l l l}
   282         -\toprule
   283         -\textbf{Treatments} & \textbf{Response 1} & \textbf{Response 2}\\
   284         -\midrule
   285         -Treatment 1 & 0.0003262 & 0.562 \\
   286         -Treatment 2 & 0.0015681 & 0.910 \\
   287         -Treatment 3 & 0.0009271 & 0.296 \\
   288         -\bottomrule
   289         -\end{tabular}
   290         -\captionof{table}{Table caption}
   291         -\end{center}
          355  +Goals in the specification logic can be \emph{executed} according to the 
          356  +traditional resolution proof search procedure. Because our logic is constructive,
          357  +the result of a successful search is not just a substitution, but also a proof
          358  +tree.
   292    359   }
   293    360   
   294    361   %----------------------------------------------------------------------------------------
   295    362   
   296    363   \end{poster}
   297    364   
   298    365   \end{document}