usecase.tex 1.57 KB
 Dennis Müller committed Apr 25, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 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} 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 11 Views have been found, the most promising of which points to the theory \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}. \begin{figure} Hier könnte Ihre Werbung stehen \caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs} \end{figure}