1 % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex
7 \setbeamercovered{transparent}
9 \usepackage[english]{babel}
10 \usepackage[latin1]{inputenc}
12 \usepackage[T1]{fontenc}
13 %\usepackage{graphicx}
15 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
16 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
18 \title[Isabelle Frontend]
19 {Userinterfaces \\f\"ur Computer Theorem Prover,\\
20 Machbarkeits-Studie im Isac-Projekt
22 \subtitle{Bachelorarbeit Telematik}
25 \institute{Institut f\"ur Software Technologie\\
26 Technische Universit\"at Graz}
29 %\subject{Formal specification of math assistants}
30 % This is only inserted into the PDF information catalog
32 % Delete this, if you do not want the table of contents to pop up at
33 % the beginning of each subsection:
38 \tableofcontents[currentsection,currentsubsection]
43 % If you wish to uncover everything in a step-wise fashion, uncomment
44 % the following command:
45 %\beamerdefaultoverlayspecification{<+->}
56 % You might wish to add the option [pausesections]
59 \section[Isabelle]{Der Theoremprover Isabelle}
61 % \frametitle{The ideal math assistant \dots}
63 %\item \alert{guides the user} step by step towards a solution\\
64 %\uncover<2->{\textit{
65 %Watching teachers calculate step by step is boring.\\
66 %Operating on formulas by hand is hard, too.\\
67 %Software can support {\bf independent learning}.
69 %\item \alert{checks user input} as generous and liberal as possible\\
70 %\uncover<3->{\textit{
71 %Active learning by {\bf trial and error} ist most effective.\\
72 %Programmers cannot foresee learners' input.\\
73 %Theorem provers provide most general checking.
75 %\item \alert{explains steps} on request by the user\\
76 %\uncover<4->{\textit{
77 %Programmers also cannot foresee learners' questions.\\
78 %A system must be {\bf transparent} for casual questions.\\
79 %LCF-style provers have knowledge human readable.
85 \frametitle{Der Theoremprover Isabelle}
87 \item Anwendungen von Isabelle
89 \item Mechanisieren von Mathematik Theorien
91 \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
92 \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots
93 \item High Order Logics, Logic of Computable Functions, \dots
95 \item Math.Grundlagen f\"ur Softwaretechnologie
97 \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
98 \item Theory for Unix file-system security, for state spaces, \dots
99 \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
102 \item Integration von Isabelle in Entwicklungstools
104 \item Boogie --- Verification Condition Generator
105 \item ? Test Case Generators (TUG) ?
108 \item Isar, die Beweissprache von Isabelle
116 \section[Komponenten]{Komponenten des kommenden Isabelle Frontends}
117 \subsection[Scala]{Scala und ``Actors''}
118 \subsection[jEdit]{jEdit und ``Plugins''}
119 \subsection[Integration]{Integration von Scala und ML}
120 \subsection[Parsen]{Parsen von Isar-Texten}
122 \section[NetBeans]{Installation der Komponenten in NetBeans}
123 \subsection[TODO]{TODO}
127 \frametitle<presentation>{Summary}