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

Florian Rabe's avatar
Florian Rabe committed
3
4
5
% Florian's macros
\usepackage{basics}

Dennis Müller's avatar
init  
Dennis Müller committed
6
\usepackage[utf8]{inputenc}
Dennis Müller's avatar
prelim    
Dennis Müller committed
7
\usepackage{url, multirow}
Dennis Müller's avatar
init  
Dennis Müller committed
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's avatar
Michael Kohlhase committed
16
\usepackage{xspace}
Dennis Müller's avatar
update    
Dennis Müller committed
17
\usepackage{mytikz}
Dennis Müller's avatar
init  
Dennis Müller committed
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's avatar
update    
Dennis Müller committed
21

Michael Kohlhase's avatar
Michael Kohlhase committed
22
23
24
25
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
Michael Kohlhase's avatar
Michael Kohlhase committed
26
\addbibresource{systems.bib}
Dennis Müller's avatar
init  
Dennis Müller committed
27
28
29
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
  \iftoggle{bbx:doi}
Michael Kohlhase's avatar
Michael Kohlhase committed
30
  {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
Dennis Müller's avatar
init  
Dennis Müller committed
31
32
33
34
    {}%
  \newunit\newblock
  \iftoggle{bbx:eprint}
    {\usebibmacro{eprint}}
Dennis Müller's avatar
Dennis Müller committed
35
    {}%froms.filterNot(t => commons.exists(_.path == t.path))
Dennis Müller's avatar
init  
Dennis Müller committed
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's avatar
Michael Kohlhase committed
44
45
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
Dennis Müller's avatar
init  
Dennis Müller committed
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's avatar
Michael Kohlhase committed
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's avatar
init  
Dennis Müller committed
59
60
61
\newif\ifshort\shorttrue

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

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

Dennis Müller's avatar
prelim    
Dennis Müller committed
66
67
\input{macros}

Florian Rabe's avatar
Florian Rabe committed
68
69
\setcounter{tocdepth}{2}

Dennis Müller's avatar
init  
Dennis Müller committed
70
71
72
73
74
\begin{document}

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


Michael Kohlhase's avatar
Michael Kohlhase committed
75
\title{Automatically Finding Theory Morphisms for Knowledge Management}
Dennis Müller's avatar
init  
Dennis Müller committed
76
\maketitle
Dennis Müller's avatar
Dennis Müller committed
77
\begin{abstract}
Michael Kohlhase's avatar
Michael Kohlhase committed
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's avatar
update    
Dennis Müller committed
88
  morphism discovery. In this paper we present an implementation in the MMT system and
Michael Kohlhase's avatar
Michael Kohlhase committed
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's avatar
Michael Kohlhase committed
92
93
\end{abstract}

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

Florian Rabe's avatar
Florian Rabe committed
97
98
\section{Preliminaries}\label{sec:prelim}
\input{prelim}
Dennis Müller's avatar
Dennis Müller committed
99

Florian Rabe's avatar
Florian Rabe committed
100
101
\section{Finding Theory Morphisms}\label{sec:viewfinder}
\input{viewfinder}
Dennis Müller's avatar
Dennis Müller committed
102

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

Dennis Müller's avatar
update    
Dennis Müller committed
106
107
108
\section{Unrealized Applications}
\input{applications}

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

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

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

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

\end{document}

%%% Local Variables:
%%% mode: latex
125
%%% eval: (visual-line-mode) (set-fill-column 5000)
Dennis Müller's avatar
init  
Dennis Müller committed
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's avatar
Michael Kohlhase committed
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's avatar
Michael Kohlhase committed
135
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
136
%  LocalWords:  usecase Unrealized