<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
The KWARC group [1] at Jacobs University Bremen [2] is looking for<br>
Ph.D. candidates and PostDocs in multiple projects, e.g. [3,4].<br>
<br>
See also <a class="moz-txt-link-freetext"
href="http://www.jacobs-university.de/jobs/phd-and-postdoc-positions-kwarc-group">http://www.jacobs-university.de/jobs/phd-and-postdoc-positions-kwarc-group</a><br>
<br>
Jacobs University Bremen is a private, English-speaking research
university in Germany.<br>
The KWARC group conducts research on the representation and
management of formal <br>
and informal knowledge in the STEM disciplines (Science, Technology,
Engineering, and Mathematics).<br>
<br>
Our interests cover the whole range from formal to informal
knowledge and include<br>
- logics and foundations of mathematics<br>
- formalizing/verifying knowledge<br>
- informal and semi-formal documents (specifications, papers, web
pages, etc.)<br>
- domain-specific applications (spreadsheets, CAD, etc.)<br>
- knowledge management (search, user interfaces, system integration,
etc.)<br>
<br>
We build systems that cover these diverse areas uniformly and
integrate across domains, languagues, and tools, always combinng
logical correctness, wide-range applicability, and large-scale
inter-operability.<br>
<br>
Interested candidates can introduce themselves or ask for further
information by email to<br>
Prof. Michael Kohlhase <a class="moz-txt-link-rfc2396E"
href="mailto:m.kohlhase@jacobs-university.de"><m.kohlhase@jacobs-university.de></a><br>
Applications (including the usual documents) should be directed to
the same email address.<br>
<br>
------------------------------<br>
<br>
We are generally flexible to develop PhD topics together with strong
candidates.<br>
Some example PhD topics that could be assigned within these
positions are given below.<br>
<br>
1) A Universal Framework for Computation<br>
<br>
Our frameworks and infrastructure are already very strong for
declarative, logical, and informal/narrative content, but lack deep
support for computational content such as programming languages,
algorithms, and libraries.<br>
Within this PhD thesis, we hope extend our OMDoc/MMT framework
toward computational content.<br>
This would in particular include case studies in the OpenDreamKit
project (e.g., programming languages like Scala or Python, computer
algebra systems like SageMath or GAP, and their libraries).<br>
<br>
2) Integrating Libraries and Databases of Mathematical Knowledge<br>
<br>
Recently computational mathematicians have built more and more
libraries of mathematical objects and models.<br>
Examples are the Online Encyclopedia of Integer Sequences (OEIS),
the FindStat library of combinatorial objects, the Library of
L-Functions and Modular Forms (LMFDB), or the Math Geneology
Project.<br>
In this PhD thesis, we want to extend our OMDoc/MMT framework with
primitives for representing such libraries uniformly as theory
graphs and extend our knowledge management algorithms to cope with
these large data volumes.<br>
<br>
3) Knowledge Management for Cognitive Enigineering<br>
<br>
Designing technical artifacts such as robots, cranes, or pens is a
knowledge-based, document-centered process (see DIN 6221).<br>
In this PhD thesis, we want to apply formal and informal knowledge
management (theory-graph) methods and active document technologies
to the engineering process and the background knowledge. We want to
build semantic sextensions to CAD systems and Office suites via our
semantic alliance framework to allow Engineers to access the
knowledge management solutions from their usual working environment.
<br>
<br>
------------------------------<br>
<br>
[1] <a class="moz-txt-link-freetext" href="http://kwarc.info">http://kwarc.info</a><br>
<br>
[2] <a class="moz-txt-link-freetext"
href="http://www.jacobs-university.de">http://www.jacobs-university.de</a><br>
<br>
[3] <a class="moz-txt-link-freetext"
href="https://kwarc.info/projects/OAF">https://kwarc.info/projects/OAF</a><br>
The Open Archive of Formalizations will provide an open
infrastructure to translate and share formalized mathematical
knowledge such as theories, definitions, and proofs between mutually
incompatible foundations (e.g., set theory, higher-order logic,
constructive type theory, etc.), library formats, and library
structures. The OAF system will be based on a uniform
foundation-independent representation format for libraries, which
allows formalizing the logical foundations alongside the libraries
and thus acts as framework for aligning libraries.<br>
<br>
[4] <a class="moz-txt-link-freetext"
href="http://opendreamkit.org/">http://opendreamkit.org/</a><br>
The Open Digital Research Environment Toolkit for the Advancement of
Mathematics will deliver a flexible toolkit enabling research groups
to set up Virtual Research Environments, customised to meet the
varied needs of research projects in pure mathematics and
applications, and supporting the full research life-cycle from
exploration, through proof and publication, to archival and sharing
of data and code, including popular tools such as LinBox, MPIR,
Sage(sagemath.org), GAP, PariGP, LMFDB, and Singular.<br>
<small> </small><br>
<pre class="moz-signature" cols="72">--
----------------------------------------------------------------------
Prof. Dr. Michael Kohlhase, Office: Research 1, Room 168
Professor of Computer Science Campus Ring 1,
Jacobs University Bremen D-28759 Bremen, Germany
tel/fax: +49 421 200-3140/-493140 skype: m.kohlhase
<a class="moz-txt-link-abbreviated" href="mailto:m.kohlhase@jacobs-university.de">m.kohlhase@jacobs-university.de</a> <a class="moz-txt-link-freetext" href="http://kwarc.info/kohlhase">http://kwarc.info/kohlhase</a>
----------------------------------------------------------------------
</pre>
</body>
</html>