Commit b6379bbe authored by Dennis Müller's avatar Dennis Müller
Browse files


parent 145841ac
......@@ -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
......@@ -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
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.
\caption{A Theory of ``Beautiful Sets'' in MMT Surface Syntax and Results of the Viewfinder}\label{fig:use:source}
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.
\caption{The Theory of Matroids in the MitM Library}\label{fig:use:target}
\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}.
Hier könnte Ihre Werbung stehen
\caption{Searching for Commutative Operators in PVS}\label{fig:use:pvs}
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment