``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
...
...
@@ -65,3 +66,22 @@ theory matroid : F?MitM
\end{tabular}
\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
\end{figure}
\paragraph{Approach and Contribution}
We have developed the MMT language \cite{RK:mmt} and the concrete syntax of the OMDoc XML format \cite{omdoc} as a uniform representation language for mathematical knowledge.
Moreover, we have exported multiple proof assistant libraries into this format, including the ones of PVS in \cite{KMOR:pvs:17} and HOL Light in \cite{RK:hollight:15}.
This enables us, for the first time, to apply generic methods --- i.e., methods that work at the MMT level --- to search for theory morphisms in these libraries.
Our contribution is twofold.
Firstly, we present such a generic theory morphism finder.\ednote{add 2 sentences about how it works}
Secondly, we apply this view finder in two concrete case studies. \ednote{add 1-2 sentences for each case study}
\paragraph{Related Work}
Existing systems have so far only worked with explicitly given theory morphisms, e.g., in IMPS \cite{imps} or Isabelle \cite{isabelle}.
Automatically and systematically searching for new theory morphisms, let alone doing so generically, is entirely novel as far as we know.
\ednote{FR: I really don't know any related work. Is there anything?}
\paragraph{Overview}
In Section~\ref{sec:prelim}, we revise the basics of MMT and the PVS and the representations of the HOL Light libraries
For the purposes of this paper, we will work with the (only slightly simplified) grammar given in Figure \ref{fig:mmtgrammar}.
...
...
@@ -43,6 +42,6 @@ We can eliminate all includes in a theory $T$ by simply copying over the constan
An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any assignment $C=t$ contained, $C$ is a constant declared in the flattened domain $T_1$ and $t$ is a syntactically well-formed term in the codomain $T_2$. We call a view \emph{total} if all \emph{undefined} constants in the domain have a corresponding assignment and \emph{partial} otherwise.
