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

structuring

parent 6b983337
``Semantic Search'' -- a very suggestive term, which is alas seriously under-defined --
has often been touted as the ``killer application'' of semantic technologies. With a view
finder, we can add another possible interpretation: searching mathematical ontologies
(here modular theorem prover libraries) at the level of theories -- we call this \defemph{theory
classification}.
The basic use case is the following: Jane, a mathematician, becomes interested in a class
of mathematical objects, say -- as a didactic example -- something she initially calls
``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
the following properties:
\begin{compactenum}
\item the empty set is beautiful over $\cB$
\item every subset of a beautiful set is beautiful over $\cB$
\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
\end{compactenum}
To see what is known about beautiful sets, she types these three conditions into a theory
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.} 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.
\begin{newpart}{MK: this could/should be extended}
In extended use cases, we could
\begin{compactitem}
\item use partial views to find theories that share significant structure with $Q$, so
that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
could just contribute a theory that extends \textsf{matroid} by a formalization of the
fourth condition -- and maybe rethink the name.
\item 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.
\end{compactitem}
\end{newpart}
\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
\begin{tabular}{|p{5cm}|p{5cm}|}\hline
$Q$ & Result \\\hline
\begin{lstlisting}[mathescape]
theory query : F?MitM
include ?set
Base : {A} set A
beautiful {A} set A $\rightarrow$ prop
empty : $\vdash$ beautiful $\emptyset$
subset-closed: $\vdash$ {}
\end{lstlisting}
&
\begin{lstlisting}[mathescape]
theory matroid : F?MitM
include ?baseset
independent {A} set A $\rightarrow$
empty: $\vdash$
hereditary : $\vdash$
augmentation: $\vdash$
\end{lstlisting}
\\\hline
\end{tabular}
\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
\end{figure}
......@@ -72,78 +72,14 @@
\end{abstract}
\setcounter{tocdepth}{2}\tableofcontents\newpage
\section{Introduction}\label{sec:intro}
\section{Applications}\label{sec:appl}
\subsection{Theory Classification}\label{sec:classifier}
``Semantic Search'' -- a very suggestive term, which is alas seriously under-defined --
has often been touted as the ``killer application'' of semantic technologies. With a view
finder, we can add another possible interpretation: searching mathematical ontologies
(here modular theorem prover libraries) at the level of theories -- we call this \defemph{theory
classification}.
The basic use case is the following: Jane, a mathematician, becomes interested in a class
of mathematical objects, say -- as a didactic example -- something she initially calls
``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
the following properties:
\begin{compactenum}
\item the empty set is beautiful over $\cB$
\item every subset of a beautiful set is beautiful over $\cB$
\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
\end{compactenum}
To see what is known about beautiful sets, she types these three conditions into a theory
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.} 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.
\begin{newpart}{MK: this could/should be extended}
In extended use cases, we could
\begin{compactitem}
\item use partial views to find theories that share significant structure with $Q$, so
that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
could just contribute a theory that extends \textsf{matroid} by a formalization of the
fourth condition -- and maybe rethink the name.
\item 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.
\end{compactitem}
\end{newpart}
\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
\begin{tabular}{|p{5cm}|p{5cm}|}\hline
$Q$ & Result \\\hline
\begin{lstlisting}[mathescape]
theory query : F?MitM
include ?set
Base : {A} set A
beautiful {A} set A $\rightarrow$ prop
empty : $\vdash$ beautiful $\emptyset$
subset-closed: $\vdash$ {}
\end{lstlisting}
&
\begin{lstlisting}[mathescape]
theory matroid : F?MitM
include ?baseset
independent {A} set A $\rightarrow$
empty: $\vdash$
hereditary : $\vdash$
augmentation: $\vdash$
\end{lstlisting}
\\\hline
\end{tabular}
\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
\end{figure}
\section{Introduction}\label{sec:intro}\input{intro}
\section{Preliminaries}\label{sec:prelim}\input{prelim}
\section{Viewfinder}\label{sec:viewfinder}\input{viewfinder}
\section{Extended Use Case}\label{sec:usecase}\input{usecase}
\section{Conclusion}\label{sec:concl}
......
MMT theories, flat, bla
\ 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