Merge branch 'master' of gl.kwarc.info:oaf/alignment-finder

tex/applications.tex

@@ -6,4 +6,7 @@
 - prioritize many definitions / theorems
 - refactoring advice
 - assoc / comm normalization
-- term indexing techniques
\ No newline at end of file
+- term indexing techniques
+- use existing views in $\cL$ (compositions of views are vivews) to give Jane more
+  information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
+  form a generalization of the notion of linear independence from linear algebra.
\ No newline at end of file

tex/intro.tex

@@ -19,13 +19,7 @@ To see what is known about beautiful sets, she types these three conditions into
 classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
 $Q$ into a library $\cL$, and returns presentations of target theories and the assignments
 made by the views. In our example we have the situation in
-Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEdit and use
-  screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
-  beautiful'', which is equivalent via the subset clause, maybe use that in the example:
-  define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
-  see what the viewfinder catches.\\
-  DM: It's not going to be a ``proper'' theorem because it will be difficult to construct a proof.
-  Apart from that it should still match Base, beautiful and the other axioms.}  In the base use case, Jane learns that her
+Figure~\ref{fig:theory-classification-ex}. In the base use case, Jane learns that her
 ``beautiful sets'' correspond to the well-known structure of
 matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
 problems.

tex/usecase.tex

+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}
\ No newline at end of file