X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fcalculemus-2003%2Fslides%2Fslides.tex;fp=helm%2Fpapers%2Fcalculemus-2003%2Fslides%2Fslides.tex;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=e7acdae5174a32bf0db182499acb128923ba7255;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/papers/calculemus-2003/slides/slides.tex b/helm/papers/calculemus-2003/slides/slides.tex deleted file mode 100644 index e7acdae51..000000000 --- a/helm/papers/calculemus-2003/slides/slides.tex +++ /dev/null @@ -1,311 +0,0 @@ - -\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}] - - 127.0.0.1 - 50004 - EqualityTactics.symmetry_tac - Hbugs_types.Use_symmetry_Luke - Use Symmetry Luke - Symmetry tutor - symmetry.environment - - \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} -