--- /dev/null
+
+\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}
+
projects / helm.git / blobdiff