Commit 8c2d086a authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

first draft of a conclusion

parent a30df950
\paragraph{Future Work} \ednote{term indexing}
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.
The latter will be important for the library refactoring and merging applications which look for all possible (partial and total) views 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
......@@ -11,3 +19,5 @@ Open Archive for Formalizations (KO 2428/13-1).
%%% eval: (visual-line-mode) (set-fill-column 5000)
%%% TeX-master: "paper"
%%% End:
% LocalWords: unrealized am:doceng10,iancu:msc Formalizations
......@@ -107,14 +107,7 @@
\input{applications}
\section{Conclusion}\label{sec:concl}
\paragraph{Future Work} \ednote{term indexing}
\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).
\input{conclusion}
\renewcommand*{\bibfont}{\small}
\printbibliography
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment