\documentclass{article}

\usepackage{a4}

\usepackage{times}

\usepackage{latexsym}

\bibliographystyle{alpha}

\usepackage{graphicx}

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

\def\Problem{ {\tt Problem }}

\title{Upcoming Userinterfaces for Computer Theorem Provers.\\

	The case of Isabelle

}

\author{G. Schafhauser, A. Schulhofer, M. Steger\\

Knowledge Management Institute (KMI)\\

TU Graz}

\begin{document}

\maketitle

\abstract{

TODO}

\section{Introduction}\label{intro} (WN)

 Computer theorem proving (CTP)\footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}, 

graphical user interfaces (GUI)

%Georg

\section{State of the art in CTP Interfaces}

\subsection{A European technology: Coq and Isabelle}\label{ctp-techn}

     http://en.wikipedia.org/wiki/Coq\\

     http://coq.inria.fr/

     http://en.wikipedia.org/wiki/Isabelle\_(theorem\_prover)\\

     http://isabelle.in.tum.de/index.html

why math -- functional: some of the languages have been specifically designed for constructing software for symbolic computation (SC). 

%+ required for \ref{ml-users}

SC http://en.wikipedia.org/wiki/Symbolic\_computation

% mainly does not compute numerical values, but terms containing variables like functions (symbols)

The LCF project

http://hopl.murdoch.edu.au/showlanguage.prx?exp=8177

specifically designed a 'meta language' (ML)

http://en.wikipedia.org/wiki/ML\_(programming\_language)

\cite{pl:milner97}

for developing CTP

\subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}

     CoqIDE, ..

         http://coq.inria.fr/what-is-coq?q=node/57\\

         earlier than Isabelle/jEdit

     ProofGeneral for Isabelle

         http://proofgeneral.inf.ed.ac.uk/\\

         emacs stone age ?

\subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir}

     @ interaction close to tty (Telegraph)\\

       BUT: separate parts in {\em one} proof could be processed in parallel

     @ http://www.informatik.uni-bremen.de/uitp/

     @ ... see\\

       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\

       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf

%Andreas

\section{Isabelle's plans for new user-interfaces}\label{gui-plans}

       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\

       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf

theorem proving will be integrated into software development

hundreds of proof obligations are generated during a software verification process 

so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE).

still many principal issues need to be clarified with respect to integration of CTP and other development tools. So engaging into details makes no sense at the present, and Isabelle will approach the final goal via experimental intermediate steps of integration.

\subsection{Connect ML-world to the users' world via JVM}\label{ml-users}

In Sect.\ref{ctp-techn} reasons have been given, why mathematics software at the state-of-the-art cannot be written in Java or the like. On the other side, Sect.\ref{gui-requir} stated requirements for mathematical user interfaces, which cannot be accomplished by ML-like languages. These requirements can be best accomplished by languages like Java, which have powerful libraries available for convenient assembly of GUIs.

\paragraph{Example: a functional mathematics engine} as the experimental one in the \sisac-project is given by the following signature:

{\it

\begin{tabbing}

\=xx\=xxxxxxxxxxxxxxxxxxxxxxxxx\=\kill

\>signature INTERPRETER =\\

\>sig\\

\>\>type calcstate\\

\>\>type step = formula * position * tactic\\

\>\> \\

\>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\

\>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\

\>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\

%\\

%\>\>val get\_next : program $\rightarrow$ calcstate $\rightarrow$ step\\

%\>\>val get\_applicable\_tactics : program $\rightarrow$ calcstate $\rightarrow$ tactic list\\

%\>\>val get\_intermediate : program $\rightarrow$ calcstate $\rightarrow$ position * position $\rightarrow$ step list\\

\>end

\end{tabbing}}

The three essential functions are \textit{do\_next}, which reads a \textit{program} for determining the next \textit{step} in a calculation, the function \textit{apply\_tactic}, which applies a \textit{tactic} input by the user to the current \textit{position} in a calculation and thus may produce a list of \textit{step}s and the function \textit{apply\_formula}, which applies an input \textit{formula} accordingly.

Now, the point with functional programming is, that the functions do {\em not} cause persistent updates in some memory, rather: all three functions above take the current state of the calculation, \textit{calcstate}, as an argument and after they have done they work return the updated \textit{calcstate}.

There are several advantages of this kind of programming: more straight forward verification, which is not discussed here, and other features. For instance, given the three functions above, it is easy to undo steps of calculations, or go back to an earlier step of calculations: one just needs to store the \textit{calcstate}s (in a list), even without knowing the details of the \textit{calcstate}, which thus can be encapsulated for internal access only.

\paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper looks like this:

TODO

\subsection{Scala as a mediator between ML and JVM}\label{scala-medi}

{\em new} language --- what for, ideas ...

\subsection{Support for parallel processing}\label{actors}

actors copied from erlang

% Marco

\section{Planned contributions at TU Graz}

\subsection{Make Isabelle process structured derivations}\label{struct-der}

Structured Derivations (SD) is a format for calculational reasoning, which has been established by \cite{back-grundy-wright-98}. This is an example calculation:

{\it\begin{tabbing}

123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill

\> $\bullet$\> \Problem [ maximum\_by, calculus ]\\

\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$\\

\>\> $\bullet$\> \Problem [make, diffable, funtion]\\

\>\> \dots\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\

\>\> $\bullet$\> \Problem [on\_interval, for\_maximum, differentiate, function]\\

\>\>\> $\vdash$\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\

\>\>\> $\bullet$\> \Problem [differentiate, funtion]\\

\>\>\> \dots\> $\overline{A}^\prime(\alpha) = 8\cdot r^2\cdot(-(\sin\alpha)^2+(\cos\alpha)^2 - 2\cdot\sin\alpha\cdot\cos\alpha)$\\

\>\>\> $\bullet$\> \Problem [on\_interval, goniometric, equation]\\

\>\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\

\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\

\>\> $\bullet$\> \Problem [tool, find\_values]\\

\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ]\\

\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !

\end{tabbing}}

The plan is to use the machinery provided Isabelle/Isar as a 'logical operating system' ~\cite{isar-impl} and adapt the machinery such that is accepts SC in parallel to the Isar proof language~\cite{wenzel:isar}.

This plan involves the following details.

\subsection{Add a plug-in to jEdit}\label{plugin}

     file structure, copied from example project ...

\subsection{Details of NetBeans projects}\label{netbeans}

     Scala + Java: html project files

\subsection{Use interfaces between Java and Scala}\label{java-scala}

     how are data exchanged between Scala and Java ...

\section{Conclusion and future work}

\bibliography{CTP-userinterfaces}

%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}

\end{document}