From 4e6d5cd52bf89e4c5d44ab86df4ef2a99b06667c Mon Sep 17 00:00:00 2001
From: Florian Rabe <florian.rabe@gmail.com>
Date: Wed, 18 Apr 2018 17:20:00 +0200
Subject: [PATCH] no message
---
tex/intro.tex | 20 ++++++++++++++++++++
tex/paper.tex | 18 +++++++++++-------
tex/prelim.tex | 7 +++----
3 files changed, 34 insertions(+), 11 deletions(-)
diff --git a/tex/intro.tex b/tex/intro.tex
index daedc46..af4ca71 100644
--- a/tex/intro.tex
+++ b/tex/intro.tex
@@ -1,3 +1,4 @@
+\paragraph{Motivation}
``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
diff --git a/tex/paper.tex b/tex/paper.tex
index 4d1b2be..0989c3b 100644
--- a/tex/paper.tex
+++ b/tex/paper.tex
@@ -63,6 +63,8 @@
\input{macros}
+\setcounter{tocdepth}{2}
+
\begin{document}
%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
@@ -87,19 +89,21 @@
avoiding duplication of work or suggesting an opportunity for refactoring.
\end{abstract}
-\setcounter{tocdepth}{2}\tableofcontents\newpage
-
-\section{Introduction}\label{sec:intro}\input{intro}
+\section{Introduction}\label{sec:intro}
+\input{intro}
-\section{Preliminaries}\label{sec:prelim}\input{prelim}
+\section{Preliminaries}\label{sec:prelim}
+\input{prelim}
-\section{Viewfinder}\label{sec:viewfinder}\input{viewfinder}
+\section{Finding Theory Morphisms}\label{sec:viewfinder}
+\input{viewfinder}
-\section{Extended Use Case}\label{sec:usecase}\input{usecase}
+\section{Applications}\label{sec:usecase}
+\input{usecase}
\section{Conclusion}\label{sec:concl}
-\subsubsection*{Acknowledgements}
+\paragraph{Acknowledgements}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Open Archive for Formalizations (KO 2428/13-1).
diff --git a/tex/prelim.tex b/tex/prelim.tex
index 0dafe61..7f29142 100644
--- a/tex/prelim.tex
+++ b/tex/prelim.tex
@@ -1,6 +1,5 @@
-MMT theories, flat, bla
-\subsection{MMT Grammar}
+\subsection{The MMT Language}
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.
-\subsection{Theory Graphs and Library Encoding}
+\subsection{Proof Assistant Libraries in MMT}
-OAF?, Meta-Theories, Logical Frameworks / LF, HOAS, Judgments-as-Types
\ No newline at end of file
+OAF: PVS, HOL Light
\ No newline at end of file
--
GitLab