paper.tex 4.65 KB
Newer Older
 Dennis Müller committed Apr 03, 2018 1 2 \documentclass[orivec]{llncs}  Florian Rabe committed Apr 26, 2018 3 4 5 % Florian's macros \usepackage{basics}  Dennis Müller committed Apr 03, 2018 6 \usepackage[utf8]{inputenc}  Dennis Müller committed Apr 17, 2018 7 \usepackage{url, multirow}  Dennis Müller committed Apr 03, 2018 8 9 10 11 12 13 14 15 %\usepackage{tipa} \usepackage{amsmath,amssymb,amstext} \usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools} \usepackage[normalem]{ulem} \usepackage{array} \usepackage{mdframed} \usepackage{wrapfig} \usepackage{paralist}  Michael Kohlhase committed Apr 04, 2018 16 \usepackage{xspace}  Dennis Müller committed Apr 25, 2018 17 \usepackage{mytikz}  Dennis Müller committed Apr 03, 2018 18 19 20 %\usepackage{appendix} \usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}  Dennis Müller committed Apr 23, 2018 21   Michael Kohlhase committed Apr 04, 2018 22 23 24 25 \addbibresource{kwarcpubs.bib} \addbibresource{extpubs.bib} \addbibresource{kwarccrossrefs.bib} \addbibresource{extcrossrefs.bib}  Michael Kohlhase committed Apr 26, 2018 26 \addbibresource{systems.bib}  Dennis Müller committed Apr 03, 2018 27 28 29 \renewbibmacro*{event+venue+date}{} \renewbibmacro*{doi+eprint+url}{% \iftoggle{bbx:doi}  Michael Kohlhase committed Apr 26, 2018 30  {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}  Dennis Müller committed Apr 03, 2018 31 32 33 34  {}% \newunit\newblock \iftoggle{bbx:eprint} {\usebibmacro{eprint}}  Dennis Müller committed Apr 13, 2018 35  {}%froms.filterNot(t => commons.exists(_.path == t.path))  Dennis Müller committed Apr 03, 2018 36 37 38 39 40 41 42 43  \newunit\newblock \iftoggle{bbx:url} {\usebibmacro{url+urldate}} {}} \setlength{\hfuzz}{3pt} \hbadness=10001 \setcounter{tocdepth}{2} % for pdf bookmarks \usepackage{xcolor}  Michael Kohlhase committed Apr 04, 2018 44 45 \usepackage{listings} \lstset{columns=fullflexible,basicstyle=\sf}  Dennis Müller committed Apr 03, 2018 46 47 48 49 50 51 52 53 \usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % local macros and configurations % \usepackage[llncs]{../../fr-macros/theorems} % \input{macros}  Michael Kohlhase committed Apr 04, 2018 54 55 56 57 58 \def\cB{\mathcal{B}} \def\cL{\mathcal{L}} \def\defemph{\textbf} \def\MMT{\textsf{MMT}\xspace} \usepackage[show]{ed}  Dennis Müller committed Apr 03, 2018 59 60 61 \newif\ifshort\shorttrue \pagestyle{plain} % remove for final version  Michael Kohlhase committed Apr 04, 2018 62   Michael Kohlhase committed Apr 15, 2018 63 \author{Dennis Müller\inst{1} \and Michael Kohlhase\inst{1}\and Florian Rabe\inst{1,2}}  Michael Kohlhase committed Apr 04, 2018 64 65 \institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}  Dennis Müller committed Apr 17, 2018 66 67 \input{macros}  Florian Rabe committed Apr 18, 2018 68 69 \setcounter{tocdepth}{2}  Dennis Müller committed Apr 03, 2018 70 71 72 73 74 \begin{document} %\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\  Michael Kohlhase committed Apr 15, 2018 75 \title{Automatically Finding Theory Morphisms for Knowledge Management}  Dennis Müller committed Apr 03, 2018 76 \maketitle  Dennis Müller committed Apr 13, 2018 77 \begin{abstract}  Michael Kohlhase committed Apr 15, 2018 78 79 80 81 82 83 84 85 86 87  We present a method for finding morphisms between formal theories, both within as well as across libraries based on different logical foundations. These morphisms can yield both (more or less formal) \emph{alignments} between individual symbols as well as truth-preserving morphisms between whole theories. As they induce new theorems in the target theory for any of the source theory, theory morphisms are high-value elements of a modular formal library. Usually, theory morphisms are manually encoded, but this practice requires authors who are familiar with source and target theories at the same time, which limits the scalability of the manual approach. To remedy this problem, we have developed a view-finder algorithm that automates theory  Dennis Müller committed Apr 25, 2018 88  morphism discovery. In this paper we present an implementation in the MMT system and  Michael Kohlhase committed Apr 15, 2018 89 90 91  show specific use cases. We focus on an application of \emph{theory discovery}, where a user can check whether a (part of a) formal theory already exists in some library, potentially avoiding duplication of work or suggesting an opportunity for refactoring.  Michael Kohlhase committed Apr 04, 2018 92 93 \end{abstract}  Florian Rabe committed Apr 18, 2018 94 95 \section{Introduction}\label{sec:intro} \input{intro}  Dennis Müller committed Apr 12, 2018 96   Florian Rabe committed Apr 18, 2018 97 98 \section{Preliminaries}\label{sec:prelim} \input{prelim}  Dennis Müller committed Apr 12, 2018 99   Florian Rabe committed Apr 18, 2018 100 101 \section{Finding Theory Morphisms}\label{sec:viewfinder} \input{viewfinder}  Dennis Müller committed Apr 12, 2018 102   Dennis Müller committed Apr 25, 2018 103 \section{Extended Use Case}\label{sec:usecase}  Florian Rabe committed Apr 18, 2018 104 \input{usecase}  Dennis Müller committed Apr 03, 2018 105   Dennis Müller committed Apr 25, 2018 106 107 108 \section{Unrealized Applications} \input{applications}  Michael Kohlhase committed Apr 04, 2018 109 \section{Conclusion}\label{sec:concl}  Dennis Müller committed Apr 03, 2018 110   Dennis Müller committed Apr 25, 2018 111 \paragraph{Future Work} \ednote{term indexing}  Dennis Müller committed Apr 18, 2018 112   Florian Rabe committed Apr 25, 2018 113 \paragraph{Acknowledgments}  Michael Kohlhase committed Apr 04, 2018 114 The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020  Michael Kohlhase committed Apr 04, 2018 115 European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An  Michael Kohlhase committed Apr 04, 2018 116 Open Archive for Formalizations (KO 2428/13-1).  Dennis Müller committed Apr 03, 2018 117 118 119 120 121 122 123 124  \renewcommand*{\bibfont}{\small} \printbibliography \end{document} %%% Local Variables: %%% mode: latex  Michael Kohlhase committed Apr 28, 2018 125 %%% eval: (visual-line-mode) (set-fill-column 5000)  Dennis Müller committed Apr 03, 2018 126 127 128 129 130 131 %%% TeX-master: t %%% End: % LocalWords: inst maketitle formalization defs well-formedness textsf sec:impl impl % LocalWords: sec:conc conc Universit printbibliography ednote Internalizing newpage  Michael Kohlhase committed Apr 04, 2018 132 133 134 % LocalWords: ifshort sec:relwork relwork renewcommand bibfont tbw setcounter tocdepth % LocalWords: tableofcontents defemph compactenum emptyset newpart compactitem lstset % LocalWords: centering aboveskip 0pt,belowskip hline lstlisting mathescape rightarrow  Michael Kohlhase committed Apr 15, 2018 135 % LocalWords: vdash baseset sec:concl subsubsection Formalizations emph sec:usecase  Michael Kohlhase committed Apr 28, 2018 136 % LocalWords: usecase Unrealized