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 was first undertaken in \cite{immanuel's paper at MKM 2006} in 2006.

Automatically and systematically searching for new theory morphisms was first undertaken in \cite{NorKoh:efnrsmk07} in 2006.

However, at that time no large corpora of formalized mathematics were available in standardized formats that would have allowed easily testing the ideas in large corpora.

This situation has changed since then as multiple such exports have become available.

...

...

@@ -73,7 +73,7 @@ In particular, we have developed the MMT language \cite{RK:mmt} and the concrete

And we have translated 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}.

Building on these developments, we are now able, 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.

While inspired by the ideas of \cite{immanuel's paper at MKM 2006}, our design and implementation are completely novel.

While inspired by the ideas of \cite{NorKoh:efnrsmk07}, our design and implementation are completely novel.

In particular, the theory makes use of the rigorous language-independent definitions of \emph{theory} and \emph{theory morphism} provided by MMT, and the practical implementation makes use of the MMT system, which provides high-level APIs for these concepts.

\cite{cezary+thibault paper} applies techniques related to ours to a related problem.

...

...

@@ -91,3 +91,8 @@ Secondly, we apply this view finder in two concrete case studies. \ednote{add 1-

\paragraph{Overview}

In Section~\ref{sec:prelim}, we revise the basics of MMT and the representations of (exemplary) the PVS and HOL Light libraries.

@@ -136,7 +136,7 @@ An assignment in a view $V:T_1\to T_2$ is syntactically well-formed if for any a

\subsection{Proof Assistant Libraries in MMT}\label{sec:oaf}

As part of the OAF project\ednote{cite}, we have imported several proof assistant libraries into the MMT system. To motivate some of the design choices made in this paper, we will outline the general procedure behind these imports.

As part of the OAF project~\cite{OAFproject:on}, we have imported several proof assistant libraries into the MMT system. To motivate some of the design choices made in this paper, we will outline the general procedure behind these imports.

\paragraph{} First, we formalize the core logical foundation of the system. We do so by using the logical framework LF\ednote{cite} (at its core a dependently-typed lambda calculus) and various extensions thereof, which are implemented in and supported by the MMT system. In LF, we can formalize the foundational primitives using the usual judgments-as-types and higher-order abstract syntax encodings -- hence theorems and axioms are represented as constants with a type $\vdash P$ for some proposition $P$, and primitive constructs like lambdas are formalized as LF-functions taking LF-lambda-expressions -- which serve as a general encoding of any variable binders -- as arguments.

...

...

@@ -188,4 +188,9 @@ The resulting formalizations are then used as meta-theory for imports of the lib

\draw[arrow](B') -- (A');

\end{tikzpicture}

\caption{A (Simplified) Theory Graph for the OAF Project}\label{fig:oaf}

Consider a corpus $C$ of theories with the same fixed meta-theory $M$.

Our goal is to find theory morphisms between them.

The cost of this problem quickly explodes.

\begin{definition}\rm

Let $C$ be a corpus of theories with the same fixed meta-theory $M$.

We call the problem of finding theory morphisms between theories of $C$ the \defemph{view finding problem} and an algorithm that solves it a \defemph{view finder}.

\end{definition}

Note that a view finder is sufficient to solve the theory classification use case from the introduction:

Jane provides a $M$-theory $Q$ of beautiful sets, the view finder computes all (total) views from $Q$ into $C$, and returns presentations of target theories and the assignments made by the views.

The cost of this problem quickly explodes.

First of all, it is advisable to restrict attention to simple morphisms.

Eventually we want to search for arbitrary morphisms as well.

But that problem is massively harder because it subsumes theorem proving: a morphism from $\Sigma$ to $\Sigma'$ maps $\Sigma$-axioms to $\Sigma'$-proofs, i.e., searching for a theory morphism requires searching for proofs.

...

...

@@ -138,4 +142,10 @@ The common logical framework used for all the libraries at our disposal makes it

\item For classical logics, we afterwards rewrite all logical connectives using their usual definitions using negation and conjunction only. Double negations are eliminated.

\item Typed Equalities are transformed to untyped ones; again getting rid of the redundant type argument of the equality.

\item The arguments of conjunctions and equalities are reordered (currently only by their number of subterms).