Commit f0ed7c92 authored by Dennis Müller's avatar Dennis Müller
Browse files

added abstract

parent fafbac5d
......@@ -29,7 +29,7 @@
{}%froms.filterNot(t => commons.exists(_.path == t.path))
......@@ -68,7 +68,16 @@
\title{Alignment Finding}
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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment