conclusion.tex 1.62 KB
Newer Older
Michael Kohlhase's avatar
Michael Kohlhase committed
1
2
3
4
5
6
7
8
We present a general MKM utility that given a \MMT theory and an \MMT library $\cL$ finds
partial and total views 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. 
Dennis Müller's avatar
update    
Dennis Müller committed
9
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. 
Michael Kohlhase's avatar
Michael Kohlhase committed
10
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}. 
Michael Kohlhase's avatar
Michael Kohlhase committed
11
12
13
14
15
16
17
18
19
20
21

\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:
Michael Kohlhase's avatar
Michael Kohlhase committed
22
23

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