helm/papers/calculemus-2003/slides/slides.tex

   1
   2 \firstslide{}
   3 % 1
   4  \begin{center}
   5   \large{\textbf{
   6     Brokers and Web-Services\\
   7     for Automatic Deduction:\\
   8     a Case Study}}
   9  \end{center}
  10  \vfill
  11  \begin{center}
  12   \small
  13   \emph{Claudio Sacerdoti Coen} \emailcsc \\
  14   \vspace{0.2cm}
  15   \tiny
  16   Department of Computer Science \\
  17   University of Bologna (Italy)
  18   \vfill
  19   \small
  20   Stefano Zacchiroli \emailzack \\
  21   \vspace{0.2cm}
  22   \tiny
  23   Department of Computer Science \\
  24   \'Ecole Normale Sup\'erieure de Paris (France)
  25  \end{center}
  26
  27 \newslide{Outline}
  28 % 2
  29  \begin{citemize}
  30   \pause
  31   \item Motivations
  32   \pause
  33   \item HELM's Proof Assistant
  34   \pause
  35   \color{blue}
  36   \item \hbugs
  37    \begin{citemize}
  38     \small
  39     \pause
  40     \item architecture
  41     \item a brief demo
  42     \item \Gray{implementation highlights (maybe)}
  43     \item future work
  44    \end{citemize}
  45  \end{citemize}
  46
  47 \newslide{Motivations}
  48 % 3
  49  Web-Service approach at software development \ldots
  50  \begin{citemize}
  51   \small
  52   \item helps in getting rid of a wide range of software incompatibilities
  53   \item is (hopefully) granted to have longevity
  54  \end{citemize}
  55  \ldots thus the WWW is moving \ldots
  56  \begin{citemize}
  57   \small
  58   \item[\Red{from}] \advirecord{f}{a disorganized repository of human-understandable
  59    HTML documents}
  60   \item[\Green{to}] \advirecord{t}{a disorganized repository of application exchanging
  61    XML documents}
  62  \end{citemize}
  63  \pause \adviplay{f} \pause \adviplay{t}
  64
  65 \newslide{Motivations}
  66 % 4
  67  The open challenge:
  68  \begin{citemize}
  69   \small
  70   \item Provide a set of stable and reliable services over this disorganization
  71  \end{citemize}
  72  \pause
  73  What about solutions? \pause \ldots \small \Red{none :-(} \pause
  74
  75  \begin{citemize}
  76   \item Just an useful architecture / widespread idea: \\
  77   \hfill add an additional intermediate level of stable services and call them
  78   \Blue{brokers}
  79  \end{citemize}
  80
  81 \newslide{\Large{HELM's Proof Assistant}}
  82 % 5
  83  \advirecord{bp}{\adviembed{display eps/helmLogic.png}}
  84  \Blue{\large Pros} \hfill \advianchor[click,underline]{bp}{\small{The Big
  85  Picture}}
  86  \begin{citemize}
  87   \small
  88   \pause
  89   \item document centric
  90   \pause
  91   \item exploits the HELM distributed library
  92    \hfill \Red{($\approx$ 40000 theorems/defs)}
  93   \pause
  94   \item modular, based on the HELM Web-Services
  95    \hfill \Red{(via XML + OMDoc)}
  96   \pause
  97   \item XML based GUI
  98    \hfill \Red{(XSLT stylesheets, MathML)}
  99   \pause
 100  \item a wonderful name: \adviwait[1] \Gray{\large{TODO}} \adviwait[1]
 101    \hfill \Red{(gTopLevel? CIClIDE?)}
 102  \end{citemize}
 103
 104 \newslide{\Large{HELM's Proof Assistant}}
 105 % 6
 106  \Blue{\large Cons}
 107  \begin{citemize}
 108   \item \Red{Beginners' Cons}
 109    \advirecord{B}{
 110     \begin{citemize}
 111      \small
 112      \item get lost in the available tactics
 113      \item focus shouldn't be on interface issues, but rather on formal proof
 114       development
 115     \end{citemize}}
 116   \item \Red{Experts' Cons}
 117    \advirecord{E}{
 118     \begin{citemize}
 119      \small
 120      \item computational expensive / resource consuming tactics
 121      \item too low exploitation of the HELM library
 122     \end{citemize}}
 123  \end{citemize}
 124  \pause \adviplay{B} \pause \adviplay{E}
 125
 126 \newslide{An improvement}
 127 % 7
 128  A \Blue{suggestion engine} that \ldots
 129  \begin{citemize}
 130   \pause
 131   \item \ldots works in background
 132   \item \ldots notify the user out-of-band
 133   \item \ldots is as much re-usable as possible
 134  \end{citemize}
 135  \vfill
 136  \begin{center}
 137   \pause \Red{\OmegaAnts}? \hspace{2cm} \pause \Blue{\hbugs}!
 138  \end{center}
 139
 140 \newslide{\hbugs{} Actors}
 141 % 8
 142  \vfill
 143  \begin{description}
 144   \item[\large{clients}]
 145    ~\advirecord{c}{\parbox[t]{0.7\textwidth}{\small Software components able to
 146    produce \Blue{proof status} consuming \Red{hints}}}
 147   \item[\large{tutors}]
 148    ~\advirecord{t}{\parbox[t]{0.7\textwidth}{\small Software components able to
 149    consume \Red{proof status} producing \Blue{hints}}}
 150   \item[\large{brokers}]
 151    ~\advirecord{b}{\parbox[t]{0.7\textwidth}{\small Software components which
 152    act as \Green{intermediaries} decoupling clients and tutors}}
 153  \end{description}
 154
 155  \pause \adviplay{c} \pause \adviplay{t} \pause \adviplay{b}
 156
 157 \newslide{\hbugs{} Architecture}
 158 % 9
 159  \vfill
 160  \myincludegraphics{hbugsArch}{0.8\textwidth}
 161
 162 \newslide{\hbugs{} Web-Services}
 163 % 10
 164  \vfill
 165  \myincludegraphics{hbugsInterfaces}{0.8\textwidth}
 166
 167 \newslide{\hbugs{} Messages}
 168 % 11
 169  \advirecord{dia}{\adviembed{dia-gnome misc/messages.dia}}
 170   \vfill
 171   \begin{center}
 172    \advianchor[click,underline]{dia}{messages.dia}
 173   \end{center}
 174
 175 \newslide{\hbugs{} Tutors}
 176 % 12
 177  \vfill
 178  \Blue{I. Tutors for beginners}
 179   \begin{enumerate}
 180    \small
 181    \item \Red{Assumption} thesis equivalent to one of the hypotheses
 182    \item \Red{Contradiction} reductio ad absurdum
 183    \item \Red{Simmetry} commutative property over equalities
 184    \item \Red{Left/Right/Exists/Split/Reflexivity/Constructor} inductive type
 185     constructors application
 186   \end{enumerate}
 187
 188 \newslide{\hbugs{} Tutors}
 189 % 13
 190  \vfill
 191  \Blue{II. Tutors for computationally expensive tactics}
 192   \begin{enumerate}
 193    \small
 194    \item \Red{Ring} associative and commutative rewritings over ring structures
 195    \item \Red{Fourier} solves linear inequation systems (over R)
 196   \end{enumerate}
 197  \vfill
 198  \pause
 199  \Blue{III. Intelligent tutors}
 200   \begin{enumerate}
 201    \small
 202    \item \Red{Search pattern Apply} search for applicable theorems from the
 203     HELM library (search + unification ``attempts'')
 204   \end{enumerate}
 205
 206 \newslide{\hbugs{} Demo}
 207 % 14
 208
 209  \vfill
 210  \begin{center}
 211   \fbox{\parbox{0.8\textwidth}{
 212   \textbf{\Red{Exercise 1.}}
 213
 214   \vspace{1cm}
 215   \emph{Let $x$ be a generic real number. Using the \helm{} proof-engine, prove
 216   that:}
 217
 218   \Blue{
 219    \begin{displaymath}
 220     x = \frac{(x+1)^2 - 1 - x^2}{2}
 221    \end{displaymath}}}}
 222  \end{center}
 223
 224 \newslide{\Large \hbugs{} Tutors' Implementation}
 225 % 15
 226  All tutors \ldots:
 227  \Blue{\begin{citemize}
 228   \small
 229   \pause
 230   \item \ldots are multi-threaded
 231   \pause
 232   \item \ldots present a Web-Service interface
 233   \pause
 234   \item \ldots perform a lot of similar operations (decoding proof status,
 235    encoding hints, parse and submit HTTP requests, \ldots)
 236  \end{citemize}}
 237
 238  \vfill
 239  \advirecord{a}{\FromRight{is not that difficult, but \ldots}}
 240
 241  \advirecord{b}{\FromRight{\Red{requires a lot of duplicated code/work :-(}}}
 242
 243  \pause \adviplay{a} \adviwait[0.5] \adviplay{b}
 244
 245 \newslide{\Large \hbugs{} Tutors' Implementation}
 246 % 16
 247  {\small To avoid the repetitive task of implementing a tutor each time we
 248  develop a new tactic:}
 249  \begin{cenumerate}
 250   \small
 251   \item[I.] ~\advirecord{a}{we have written a \Green{generic tutor
 252    implementation}}
 253   \item[II.] ~\advirecord{b}{we \Green{instantiate} it with each available tactic
 254    starting from an XML signature of each tutor}
 255    \begin{Verbatim}[fontshape=it,fontsize=\tiny,formatcom=\color{blue}]
 256     <tutor source="symmetry_tutor.ml">
 257       <addr>127.0.0.1</addr>
 258       <port>50004</port>
 259       <tactic>EqualityTactics.symmetry_tac</tactic>
 260       <hint>Hbugs_types.Use_symmetry_Luke</hint>
 261       <hint_type>Use Symmetry Luke</hint_type>
 262       <description>Symmetry tutor</description>
 263       <environment_file>symmetry.environment</environment_file>
 264     </tutor>
 265    \end{Verbatim}
 266  \end{cenumerate}
 267  \pause \adviplay{a} \pause \adviplay{b}
 268
 269 \newslide{\hbugs{} Future Work}
 270 % 17
 271  \vfill
 272  \begin{center}
 273   \Blue{\Large{A lot!}}
 274  \end{center}
 275  \vfill
 276  \begin{citemize}
 277   \item ~\advirecord{a}{implement more \advirecord{b}{\Gray{(Intelligent)}}
 278    tutors}
 279   \item ~\advirecord{c}{interfacing of CASs \hfill \Red{(Field tactic?)}}
 280   \item ~\advirecord{d}{non-hint \hfill \Red{(warnings?)}}
 281   \item ~\advirecord{e}{hints rating}
 282   \item ~\advirecord{f}{MONET integration \hfill \Red{ontologies, reuse}}
 283   \item ~\advirecord{g}{work on the GUI!}
 284  \end{citemize}
 285
 286  \pause \adviplay{a} \adviwait[0.3] \adviplay{b} \pause \adviplay{c} \pause
 287  \adviplay{d} \pause \adviplay{e} \pause \adviplay{f} \pause \adviplay{g}
 288
 289 \newslide{References}
 290 % 18
 291  \vfill
 292  \begin{citemize}
 293   \item A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
 294   Mathematical Knowledge Management in HELM. In Annals of Mathematics and
 295   Artificial Intelligence, 38(1): 27--46, May 2003.
 296   \item C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
 297   Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
 298   Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
 299   \item The MONET Consortium, MONET Architecture Overview,
 300   Public Deliverable D04 of the MONET Project.\\
 301   \texttt{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
 302   \item S. Zacchiroli. \emph{Web services per il supporto alla
 303   dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
 304  \end{citemize}
 305
 306 \newslide{That's all Folks!}
 307 % 19
 308  \vfill
 309  \adviwait[1]
 310  \myincludegraphics{thatsall}{0.4\textwidth}
 311