Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
OAF
alignment-finder
Commits
f0581576
Commit
f0581576
authored
Apr 15, 2018
by
Michael Kohlhase
Browse files
adapting title/abstract
parent
f0ed7c92
Changes
1
Hide whitespace changes
Inline
Side-by-side
tex/paper.tex
View file @
f0581576
...
...
@@ -58,7 +58,7 @@
\pagestyle
{
plain
}
% remove for final version
\author
{
Dennis Müller
\inst
{
1
}
\and
Florian Rab
e
\inst
{
1
,2
}
\and
Michael Kohlhas
e
\inst
{
1
}}
\author
{
Dennis Müller
\inst
{
1
}
\and
Michael Kohlhas
e
\inst
{
1
}
\and
Florian Rab
e
\inst
{
1
,2
}}
\institute
{
Computer Science, FAU Erlangen-N
\"
urnberg
\and
LRI, Universit
\'
e Paris Sud
}
\begin{document}
...
...
@@ -66,18 +66,23 @@
%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
\title
{
A
lignment Finding
}
\title
{
A
utomatically 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.
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.
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}
\setcounter
{
tocdepth
}{
2
}
\tableofcontents\newpage
...
...
@@ -113,4 +118,5 @@ Open Archive for Formalizations (KO 2428/13-1).
% 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
% LocalWords: vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
% LocalWords: usecase
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment