paper.tex 4.04 KB
Newer Older
Dennis Müller's avatar
init  
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
\documentclass[orivec]{llncs}

\usepackage[utf8]{inputenc}
\usepackage{url}
%\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
61
62
63

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

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

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


\title{Alignment Finding}
\maketitle
Dennis Müller's avatar
Dennis Müller committed
71
72
73
74
75
76
77
78
79
80
\begin{abstract}
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. 

In particular, 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.

Furthermore, we present an implementation of both the algorithm as well as the specific use case in the MMT system.
Michael Kohlhase's avatar
Michael Kohlhase committed
81
82
83
\end{abstract}

\setcounter{tocdepth}{2}\tableofcontents\newpage
Dennis Müller's avatar
Dennis Müller committed
84
85
86
87
88
89
90
91

\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
92

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

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

\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
113
114
115
116
%  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
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations