paper.tex 4.48 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

Dennis Müller's avatar
Dennis Müller committed
22
23
24
25
26
27
%\addbibresource{kwarcpubs.bib}
%\addbibresource{extpubs.bib}
%\addbibresource{kwarccrossrefs.bib}
%\addbibresource{extcrossrefs.bib}
%\addbibresource{systems.bib}
\addbibresource{biblio}
Dennis Müller's avatar
init  
Dennis Müller committed
28
29
30
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
  \iftoggle{bbx:doi}
Michael Kohlhase's avatar
Michael Kohlhase committed
31
  {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
Dennis Müller's avatar
init  
Dennis Müller committed
32
33
34
35
    {}%
  \newunit\newblock
  \iftoggle{bbx:eprint}
    {\usebibmacro{eprint}}
Dennis Müller's avatar
Dennis Müller committed
36
    {}%froms.filterNot(t => commons.exists(_.path == t.path))
Dennis Müller's avatar
init  
Dennis Müller committed
37
38
39
40
41
42
43
44
  \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
45
46
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
Dennis Müller's avatar
init  
Dennis Müller committed
47
48
49
50
51
52
53
54
\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
55
56
57
58
59
\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
60
61
62
\newif\ifshort\shorttrue

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

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

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

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

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

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


Michael Kohlhase's avatar
Michael Kohlhase committed
76
\title{Automatically Finding Theory Morphisms for Knowledge Management}
Dennis Müller's avatar
init  
Dennis Müller committed
77
\maketitle
Dennis Müller's avatar
Dennis Müller committed
78
\begin{abstract}
Michael Kohlhase's avatar
Michael Kohlhase committed
79
  We present a method for finding morphisms between formal theories, both within as well
Dennis Müller's avatar
Dennis Müller committed
80
81
82
  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
Michael Kohlhase's avatar
Michael Kohlhase committed
83
84
85
86
  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. 

Florian Rabe's avatar
Florian Rabe committed
87
  To remedy this problem, we have developed a morphism 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}
Michael Kohlhase's avatar
Michael Kohlhase committed
96

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

Florian Rabe's avatar
Florian Rabe committed
100
\section{Intra-Library View Finding}\label{sec:viewfinder}
Florian Rabe's avatar
Florian Rabe committed
101
\input{viewfinder}
Dennis Müller's avatar
Dennis Müller committed
102

Florian Rabe's avatar
Florian Rabe committed
103
\section{Inter-Library View Finding}\label{sec:across}
Florian Rabe's avatar
Florian Rabe committed
104
\input{usecase}
Dennis Müller's avatar
init  
Dennis Müller committed
105

Michael Kohlhase's avatar
title    
Michael Kohlhase committed
106
\section{Low-Hanging Fruit: Other Applications}\label{sec:appl}
Dennis Müller's avatar
update    
Dennis Müller committed
107
108
\input{applications}

Michael Kohlhase's avatar
Michael Kohlhase committed
109
\section{Conclusion}\label{sec:concl}
Michael Kohlhase's avatar
Michael Kohlhase committed
110
\input{conclusion}
Florian Rabe's avatar
Florian Rabe committed
111

Dennis Müller's avatar
init  
Dennis Müller committed
112
113
114
115
116
117
118
\renewcommand*{\bibfont}{\small}
\printbibliography

\end{document}

%%% Local Variables:
%%% mode: latex
Michael Kohlhase's avatar
Michael Kohlhase committed
119
120
%%% eval:  (set-fill-column 5000)
%%% eval:  (visual-line-mode)
Dennis Müller's avatar
init  
Dennis Müller committed
121
122
123
124
125
126
%%% 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
127
128
129
%  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
130
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
Michael Kohlhase's avatar
Michael Kohlhase committed
131
%  LocalWords:  usecase Unrealized sec:appl