+++ /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