conclusion.tex

We present a general MKM utility that given a \MMT theory and an \MMT library $\cL$ finds
partial and total morphisms into $\cL$.  
Such a view finder can be used to drive various MKM applications ranging from theory classification to library merging and refactoring. 
We have presented the first and last of these and show that they are feasible. For the applications discussed but unrealized in this paper, we mainly need to determine the right application context and user interface. 
 
\paragraph{Future Work} 
The current view finder is already efficient enough for the limited libraries we used for testing. 
To increase efficiency, we plan to explore term indexing techniques~\cite{Graf:ti96} that support $1:n$ and even $n:m$ matching and unification queries. 
The latter will be important for the library refactoring and merging applications which look for all possible (partial and total) morphisms in one or between two libraries. 
As such library-scale operations will have to be run together with theory flattening to a fixed point and re-run upon every addition to the library, it will be important to integrate them with the \MMT build system and change management processes~\cite{am:doceng10,iancu:msc}. 

\paragraph{Acknowledgments}
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).

%%% Local Variables:
%%% mode: latex
%%% eval: (visual-line-mode) (set-fill-column 5000) 
%%% TeX-master: "paper"
%%% End:

%  LocalWords:  unrealized am:doceng10,iancu:msc Formalizations