paper.tex 4.56 KB
Newer Older
Dennis Müller's avatar
init  
Dennis Müller committed
1
2
3
\documentclass[orivec]{llncs}

\usepackage[utf8]{inputenc}
Dennis Müller's avatar
prelim    
Dennis Müller committed
4
\usepackage{url, multirow}
Dennis Müller's avatar
init  
Dennis Müller committed
5
6
7
8
9
10
11
12
%\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's avatar
Michael Kohlhase committed
13
\usepackage{xspace}
Dennis Müller's avatar
update    
Dennis Müller committed
14
\usepackage{mytikz}
Dennis Müller's avatar
init  
Dennis Müller committed
15
16
17
%\usepackage{appendix}

\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
Dennis Müller's avatar
update    
Dennis Müller committed
18

Michael Kohlhase's avatar
Michael Kohlhase committed
19
20
21
22
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
Dennis Müller's avatar
init  
Dennis Müller committed
23
24
25
26
27
28
29
30
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
  \iftoggle{bbx:doi}
    {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
    {}%
  \newunit\newblock
  \iftoggle{bbx:eprint}
    {\usebibmacro{eprint}}
Dennis Müller's avatar
Dennis Müller committed
31
    {}%froms.filterNot(t => commons.exists(_.path == t.path))
Dennis Müller's avatar
init  
Dennis Müller committed
32
33
34
35
36
37
38
39
  \newunit\newblock
  \iftoggle{bbx:url}
    {\usebibmacro{url+urldate}}
    {}}

\setlength{\hfuzz}{3pt} \hbadness=10001
\setcounter{tocdepth}{2} % for pdf bookmarks
\usepackage{xcolor}
Michael Kohlhase's avatar
Michael Kohlhase committed
40
41
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
Dennis Müller's avatar
init  
Dennis Müller committed
42
43
44
45
46
47
48
49
50
\usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% local macros and configurations

% \usepackage{../../fr-macros/basics}
% \usepackage[llncs]{../../fr-macros/theorems}
% \input{macros}

Michael Kohlhase's avatar
Michael Kohlhase committed
51
52
53
54
55
\def\cB{\mathcal{B}}
\def\cL{\mathcal{L}}
\def\defemph{\textbf}
\def\MMT{\textsf{MMT}\xspace}
\usepackage[show]{ed}
Dennis Müller's avatar
init  
Dennis Müller committed
56
57
58
\newif\ifshort\shorttrue

\pagestyle{plain} % remove for final version
Michael Kohlhase's avatar
Michael Kohlhase committed
59

Michael Kohlhase's avatar
Michael Kohlhase committed
60
\author{Dennis Müller\inst{1} \and Michael Kohlhase\inst{1}\and Florian Rabe\inst{1,2}}
Michael Kohlhase's avatar
Michael Kohlhase committed
61
62
\institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}

Dennis Müller's avatar
prelim    
Dennis Müller committed
63
64
\input{macros}

Florian Rabe's avatar
Florian Rabe committed
65
66
\setcounter{tocdepth}{2}

Dennis Müller's avatar
init  
Dennis Müller committed
67
68
69
70
71
\begin{document}

%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\


Michael Kohlhase's avatar
Michael Kohlhase committed
72
\title{Automatically Finding Theory Morphisms for Knowledge Management}
Dennis Müller's avatar
init  
Dennis Müller committed
73
\maketitle
Dennis Müller's avatar
Dennis Müller committed
74
\begin{abstract}
Michael Kohlhase's avatar
Michael Kohlhase committed
75
76
77
78
79
80
81
82
83
84
  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's avatar
update    
Dennis Müller committed
85
  morphism discovery. In this paper we present an implementation in the MMT system and
Michael Kohlhase's avatar
Michael Kohlhase committed
86
87
88
  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's avatar
Michael Kohlhase committed
89
90
\end{abstract}

Florian Rabe's avatar
Florian Rabe committed
91
92
\section{Introduction}\label{sec:intro}
\input{intro}
Dennis Müller's avatar
Dennis Müller committed
93

Florian Rabe's avatar
Florian Rabe committed
94
95
\section{Preliminaries}\label{sec:prelim}
\input{prelim}
Dennis Müller's avatar
Dennis Müller committed
96

Florian Rabe's avatar
Florian Rabe committed
97
98
\section{Finding Theory Morphisms}\label{sec:viewfinder}
\input{viewfinder}
Dennis Müller's avatar
Dennis Müller committed
99

Dennis Müller's avatar
update    
Dennis Müller committed
100
\section{Extended Use Case}\label{sec:usecase}
Florian Rabe's avatar
Florian Rabe committed
101
\input{usecase}
Dennis Müller's avatar
init  
Dennis Müller committed
102

Dennis Müller's avatar
update    
Dennis Müller committed
103
104
105
\section{Unrealized Applications}
\input{applications}

Michael Kohlhase's avatar
Michael Kohlhase committed
106
\section{Conclusion}\label{sec:concl}
Dennis Müller's avatar
init  
Dennis Müller committed
107

Dennis Müller's avatar
update    
Dennis Müller committed
108
\paragraph{Future Work} \ednote{term indexing}
Dennis Müller's avatar
update    
Dennis Müller committed
109

Florian Rabe's avatar
Florian Rabe committed
110
\paragraph{Acknowledgments}
Michael Kohlhase's avatar
Michael Kohlhase committed
111
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
Michael Kohlhase's avatar
Michael Kohlhase committed
112
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Michael Kohlhase's avatar
Michael Kohlhase committed
113
Open Archive for Formalizations (KO 2428/13-1).
Dennis Müller's avatar
init  
Dennis Müller committed
114
115
116
117
118
119
120
121
122
123
124
125
126
127

\renewcommand*{\bibfont}{\small}
\printbibliography

\end{document}

%%% Local Variables:
%%% mode: latex
%%% 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's avatar
Michael Kohlhase committed
128
129
130
%  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's avatar
Michael Kohlhase committed
131
132
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
%  LocalWords:  usecase