usecase.tex 1.77 KB
 Dennis Müller committed Apr 25, 2018 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 committed Apr 25, 2018 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 committed Apr 25, 2018 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 committed Apr 25, 2018 21 22 \begin{figure}[ht]\centering \fbox{\includegraphics[width=\textwidth]{pvs}} Dennis Müller committed Apr 25, 2018 23 \caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs} Dennis Müller committed Apr 26, 2018 24 \end{figure} Michael Kohlhase committed Apr 28, 2018 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