
\firstslide{}
% 1
 \begin{center}
  \large{\textbf{
    Brokers and Web-Services\\
    for Automatic Deduction:\\
    a Case Study}}
 \end{center}
 \vfill
 \begin{center}
  \small
  \emph{Claudio Sacerdoti Coen} \emailcsc \\
  \vspace{0.2cm}
  \tiny
  Department of Computer Science \\
  University of Bologna (Italy)
  \vfill
  \small
  Stefano Zacchiroli \emailzack \\
  \vspace{0.2cm}
  \tiny
  Department of Computer Science \\
  \'Ecole Normale Sup\'erieure de Paris (France)
 \end{center}

\newslide{Outline}
% 2
 \begin{citemize}
  \pause
  \item Motivations
  \pause
  \item HELM's Proof Assistant
  \pause
  \color{blue}
  \item \hbugs
   \begin{citemize}
    \small
    \pause
    \item architecture
    \item a brief demo
    \item \Gray{implementation highlights (maybe)}
    \item future work
   \end{citemize}
 \end{citemize}

\newslide{Motivations}
% 3
 Web-Service approach at software development \ldots
 \begin{citemize}
  \small
  \item helps in getting rid of a wide range of software incompatibilities
  \item is (hopefully) granted to have longevity
 \end{citemize}
 \ldots thus the WWW is moving \ldots
 \begin{citemize}
  \small
  \item[\Red{from}] \advirecord{f}{a disorganized repository of human-understandable
   HTML documents}
  \item[\Green{to}] \advirecord{t}{a disorganized repository of application exchanging
   XML documents}
 \end{citemize}
 \pause \adviplay{f} \pause \adviplay{t}

\newslide{Motivations}
% 4
 The open challenge:
 \begin{citemize}
  \small
  \item Provide a set of stable and reliable services over this disorganization
 \end{citemize}
 \pause
 What about solutions? \pause \ldots \small \Red{none :-(} \pause

 \begin{citemize}
  \item Just an useful architecture / widespread idea: \\
  \hfill add an additional intermediate level of stable services and call them
  \Blue{brokers}
 \end{citemize}

\newslide{\Large{HELM's Proof Assistant}}
% 5
 \advirecord{bp}{\adviembed{display eps/helmLogic.png}}
 \Blue{\large Pros} \hfill \advianchor[click,underline]{bp}{\small{The Big
 Picture}}
 \begin{citemize}
  \small
  \pause
  \item document centric
  \pause
  \item exploits the HELM distributed library
   \hfill \Red{($\approx$ 40000 theorems/defs)}
  \pause
  \item modular, based on the HELM Web-Services
   \hfill \Red{(via XML + OMDoc)}
  \pause
  \item XML based GUI
   \hfill \Red{(XSLT stylesheets, MathML)}
  \pause
 \item a wonderful name: \adviwait[1] \Gray{\large{TODO}} \adviwait[1]
   \hfill \Red{(gTopLevel? CIClIDE?)}
 \end{citemize}

\newslide{\Large{HELM's Proof Assistant}}
% 6
 \Blue{\large Cons}
 \begin{citemize}
  \item \Red{Beginners' Cons}
   \advirecord{B}{
    \begin{citemize}
     \small
     \item get lost in the available tactics
     \item focus shouldn't be on interface issues, but rather on formal proof
      development
    \end{citemize}}
  \item \Red{Experts' Cons}
   \advirecord{E}{
    \begin{citemize}
     \small
     \item computational expensive / resource consuming tactics
     \item too low exploitation of the HELM library
    \end{citemize}}
 \end{citemize}
 \pause \adviplay{B} \pause \adviplay{E}

\newslide{An improvement}
% 7
 A \Blue{suggestion engine} that \ldots
 \begin{citemize}
  \pause
  \item \ldots works in background
  \item \ldots notify the user out-of-band
  \item \ldots is as much re-usable as possible
 \end{citemize}
 \vfill
 \begin{center}
  \pause \Red{\OmegaAnts}? \hspace{2cm} \pause \Blue{\hbugs}!
 \end{center}

\newslide{\hbugs{} Actors}
% 8
 \vfill
 \begin{description}
  \item[\large{clients}]
   ~\advirecord{c}{\parbox[t]{0.7\textwidth}{\small Software components able to
   produce \Blue{proof status} consuming \Red{hints}}}
  \item[\large{tutors}]
   ~\advirecord{t}{\parbox[t]{0.7\textwidth}{\small Software components able to
   consume \Red{proof status} producing \Blue{hints}}}
  \item[\large{brokers}]
   ~\advirecord{b}{\parbox[t]{0.7\textwidth}{\small Software components which
   act as \Green{intermediaries} decoupling clients and tutors}}
 \end{description}

 \pause \adviplay{c} \pause \adviplay{t} \pause \adviplay{b}

\newslide{\hbugs{} Architecture}
% 9
 \vfill
 \myincludegraphics{hbugsArch}{0.8\textwidth}

\newslide{\hbugs{} Web-Services}
% 10
 \vfill
 \myincludegraphics{hbugsInterfaces}{0.8\textwidth}

\newslide{\hbugs{} Messages}
% 11
 \advirecord{dia}{\adviembed{dia-gnome misc/messages.dia}}
  \vfill
  \begin{center}
   \advianchor[click,underline]{dia}{messages.dia}
  \end{center}

\newslide{\hbugs{} Tutors}
% 12
 \vfill
 \Blue{I. Tutors for beginners}
  \begin{enumerate}
   \small
   \item \Red{Assumption} thesis equivalent to one of the hypotheses
   \item \Red{Contradiction} reductio ad absurdum
   \item \Red{Simmetry} commutative property over equalities
   \item \Red{Left/Right/Exists/Split/Reflexivity/Constructor} inductive type
    constructors application
  \end{enumerate}

\newslide{\hbugs{} Tutors}
% 13
 \vfill
 \Blue{II. Tutors for computationally expensive tactics}
  \begin{enumerate}
   \small
   \item \Red{Ring} associative and commutative rewritings over ring structures
   \item \Red{Fourier} solves linear inequation systems (over R)
  \end{enumerate}
 \vfill
 \pause
 \Blue{III. Intelligent tutors}
  \begin{enumerate}
   \small
   \item \Red{Search pattern Apply} search for applicable theorems from the
    HELM library (search + unification ``attempts'')
  \end{enumerate}

\newslide{\hbugs{} Demo}
% 14

 \vfill
 \begin{center}
  \fbox{\parbox{0.8\textwidth}{
  \textbf{\Red{Exercise 1.}}

  \vspace{1cm}
  \emph{Let $x$ be a generic real number. Using the \helm{} proof-engine, prove
  that:}

  \Blue{
   \begin{displaymath}
    x = \frac{(x+1)^2 - 1 - x^2}{2}
   \end{displaymath}}}}
 \end{center}

\newslide{\Large \hbugs{} Tutors' Implementation}
% 15
 All tutors \ldots:
 \Blue{\begin{citemize}
  \small
  \pause
  \item \ldots are multi-threaded
  \pause
  \item \ldots present a Web-Service interface
  \pause
  \item \ldots perform a lot of similar operations (decoding proof status,
   encoding hints, parse and submit HTTP requests, \ldots)
 \end{citemize}}

 \vfill 
 \advirecord{a}{\FromRight{is not that difficult, but \ldots}}

 \advirecord{b}{\FromRight{\Red{requires a lot of duplicated code/work :-(}}}

 \pause \adviplay{a} \adviwait[0.5] \adviplay{b}

\newslide{\Large \hbugs{} Tutors' Implementation}
% 16
 {\small To avoid the repetitive task of implementing a tutor each time we
 develop a new tactic:}
 \begin{cenumerate}
  \small
  \item[I.] ~\advirecord{a}{we have written a \Green{generic tutor
   implementation}}
  \item[II.] ~\advirecord{b}{we \Green{instantiate} it with each available tactic
   starting from an XML signature of each tutor}
   \begin{Verbatim}[fontshape=it,fontsize=\tiny,formatcom=\color{blue}]
    <tutor source="symmetry_tutor.ml">
      <addr>127.0.0.1</addr>
      <port>50004</port>
      <tactic>EqualityTactics.symmetry_tac</tactic>
      <hint>Hbugs_types.Use_symmetry_Luke</hint>
      <hint_type>Use Symmetry Luke</hint_type>
      <description>Symmetry tutor</description>
      <environment_file>symmetry.environment</environment_file>
    </tutor>
   \end{Verbatim}
 \end{cenumerate}
 \pause \adviplay{a} \pause \adviplay{b}

\newslide{\hbugs{} Future Work}
% 17
 \vfill
 \begin{center}
  \Blue{\Large{A lot!}}
 \end{center}
 \vfill
 \begin{citemize}
  \item ~\advirecord{a}{implement more \advirecord{b}{\Gray{(Intelligent)}}
   tutors}
  \item ~\advirecord{c}{interfacing of CASs \hfill \Red{(Field tactic?)}}
  \item ~\advirecord{d}{non-hint \hfill \Red{(warnings?)}}
  \item ~\advirecord{e}{hints rating}
  \item ~\advirecord{f}{MONET integration \hfill \Red{ontologies, reuse}}
  \item ~\advirecord{g}{work on the GUI!}
 \end{citemize}

 \pause \adviplay{a} \adviwait[0.3] \adviplay{b} \pause \adviplay{c} \pause
 \adviplay{d} \pause \adviplay{e} \pause \adviplay{f} \pause \adviplay{g}

\newslide{References}
% 18
 \vfill
 \begin{citemize}
  \item A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
  Mathematical Knowledge Management in HELM. In Annals of Mathematics and
  Artificial Intelligence, 38(1): 27--46, May 2003.
  \item C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
  Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
  Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
  \item The MONET Consortium, MONET Architecture Overview,
  Public Deliverable D04 of the MONET Project.\\
  \texttt{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
  \item S. Zacchiroli. \emph{Web services per il supporto alla
  dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
 \end{citemize}

\newslide{That's all Folks!}
% 19
 \vfill
 \adviwait[1]
 \myincludegraphics{thatsall}{0.4\textwidth}

