paper.tex 4.58 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
init  
Dennis Müller committed
14
15
16
17
18
19
%\usepackage{appendix}

\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
% \addbibresource{../../fr-macros/rabe.bib}
% \addbibresource{../../fr-macros/systems.bib}
% \addbibresource{../../fr-macros/pub_rabe.bib}
Michael Kohlhase's avatar
Michael Kohlhase committed
20
21
22
23
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
Dennis Müller's avatar
init  
Dennis Müller committed
24
25
26
27
28
29
30
31
\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
32
    {}%froms.filterNot(t => commons.exists(_.path == t.path))
Dennis Müller's avatar
init  
Dennis Müller committed
33
34
35
36
37
38
39
40
  \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
41
42
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
Dennis Müller's avatar
init  
Dennis Müller committed
43
44
45
46
47
48
49
50
51
\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
52
53
54
55
56
\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
57
58
59
\newif\ifshort\shorttrue

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

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

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

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

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


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

\setcounter{tocdepth}{2}\tableofcontents\newpage
Dennis Müller's avatar
Dennis Müller committed
91
92
93
94
95
96
97
98

\section{Introduction}\label{sec:intro}\input{intro}

\section{Preliminaries}\label{sec:prelim}\input{prelim}

\section{Viewfinder}\label{sec:viewfinder}\input{viewfinder}

\section{Extended Use Case}\label{sec:usecase}\input{usecase}
Dennis Müller's avatar
init  
Dennis Müller committed
99

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

Michael Kohlhase's avatar
Michael Kohlhase committed
102
103
\subsubsection*{Acknowledgements}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
Michael Kohlhase's avatar
Michael Kohlhase committed
104
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Michael Kohlhase's avatar
Michael Kohlhase committed
105
Open Archive for Formalizations (KO 2428/13-1).
Dennis Müller's avatar
init  
Dennis Müller committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119

\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
120
121
122
%  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
123
124
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
%  LocalWords:  usecase