usecase.tex 1.77 KB
Newer Older
Dennis Müller's avatar
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
The Viewfinder algorithm is implemented in the MMT system and exposed within the jEdit-IDE, allowing us to realize the use case
stated in the introduction. A screenshot of Jane's theory of beautiful sets is given in Figure \ref{fig:use:source}; it
is based on the (basic higher-order logic) foundation of the Math-in-the-Middle\ednote{cite} library developed natively in MMT.

\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=0.6\textwidth]{beautysource}}
  \fbox{\includegraphics[width=\textwidth]{results}}
\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the Viewfinder}\label{fig:use:source}
\end{figure}

Dennis Müller's avatar
Update    
Dennis Müller committed
11
Right-clicking anywhere within the theory allows Jane to select \cn{MMT} $\to$ \cn{Find\ Views\ to...} $\to$ \cn{MitM/smglom} (the main Math-in-the-Middle library), telling her (within less than one second) that two views have been found, the most promising of which points to the theory
Dennis Müller's avatar
Dennis Müller committed
12
13
14
15
16
17
18
19
20
\cn{matroid\_theory} (see Figure \ref{fig:use:target}) in the library.

\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=0.6\textwidth]{matroids}}
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}
\end{figure}

\paragraph{} Using a different library as target, we can for example quickly write down a theory for a commutative binary operator (still using the Math-in-the-Middle foundation), allowing us to search e.g. the PVS Prelude library for any commutative operators, as in Figure \ref{fig:use:pvs}.

Dennis Müller's avatar
Update    
Dennis Müller committed
21
22
\begin{figure}[ht]\centering
  \fbox{\includegraphics[width=\textwidth]{pvs}}
Dennis Müller's avatar
Dennis Müller committed
23
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
Dennis Müller's avatar
adnote    
Dennis Müller committed
24
\end{figure}
25
26
\ednote{8 results for NASA, but NASA doesn't work in jEdit because of limited memory}
%  LocalWords:  ednote centering fbox includegraphics textwidth beautysource smglom pvs