paper.tex

\documentclass[orivec]{llncs}

\usepackage[utf8]{inputenc}
\usepackage{url, multirow}
%\usepackage{tipa}
\usepackage{amsmath,amssymb,amstext}
\usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools}
\usepackage[normalem]{ulem}
\usepackage{array}
\usepackage{mdframed}
\usepackage{wrapfig}
\usepackage{paralist}
\usepackage{xspace}
%\usepackage{appendix}

\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}

\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
  \iftoggle{bbx:doi}
    {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
    {}%
  \newunit\newblock
  \iftoggle{bbx:eprint}
    {\usebibmacro{eprint}}
    {}%froms.filterNot(t => commons.exists(_.path == t.path))
  \newunit\newblock
  \iftoggle{bbx:url}
    {\usebibmacro{url+urldate}}
    {}}

\setlength{\hfuzz}{3pt} \hbadness=10001
\setcounter{tocdepth}{2} % for pdf bookmarks
\usepackage{xcolor}
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
\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}

\def\cB{\mathcal{B}}
\def\cL{\mathcal{L}}
\def\defemph{\textbf}
\def\MMT{\textsf{MMT}\xspace}
\usepackage[show]{ed}
\newif\ifshort\shorttrue

\pagestyle{plain} % remove for final version

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

\input{macros}

\setcounter{tocdepth}{2}

\begin{document}

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


\title{Automatically Finding Theory Morphisms for Knowledge Management}
\maketitle
\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. 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.
\end{abstract}

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

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

\section{Finding Theory Morphisms}\label{sec:viewfinder}
\input{viewfinder}

\section{Applications}\label{sec:usecase}
\input{usecase}

\section{Conclusion}\label{sec:concl}

\paragraph{Future Work} \ednote{term indexing, normalization, using alignments / translations between libraries}

\paragraph{Acknowledgements}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Open Archive for Formalizations (KO 2428/13-1).

\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
%  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 emph sec:usecase
%  LocalWords:  usecase