The KWARC group [1] at Jacobs University Bremen [2] is looking for Ph.D. candidates and PostDocs in multiple projects, e.g. [3,4]. See also http://www.jacobs-university.de/jobs/phd-and-postdoc-positions-kwarc-group Jacobs University Bremen is a private, English-speaking research university in Germany. The KWARC group conducts research on the representation and management of formal and informal knowledge in the STEM disciplines (Science, Technology, Engineering, and Mathematics). Our interests cover the whole range from formal to informal knowledge and include - logics and foundations of mathematics - formalizing/verifying knowledge - informal and semi-formal documents (specifications, papers, web pages, etc.) - domain-specific applications (spreadsheets, CAD, etc.) - knowledge management (search, user interfaces, system integration, etc.) 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. Interested candidates can introduce themselves or ask for further information by email to Prof. Michael Kohlhase <m.kohlhase@jacobs-university.de> Applications (including the usual documents) should be directed to the same email address. ------------------------------ We are generally flexible to develop PhD topics together with strong candidates. Some example PhD topics that could be assigned within these positions are given below. 1) A Universal Framework for Computation 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. Within this PhD thesis, we hope extend our OMDoc/MMT framework toward computational content. 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). 2) Integrating Libraries and Databases of Mathematical Knowledge Recently computational mathematicians have built more and more libraries of mathematical objects and models. 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. 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. 3) Knowledge Management for Cognitive Enigineering Designing technical artifacts such as robots, cranes, or pens is a knowledge-based, document-centered process (see DIN 6221). 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. ------------------------------ [1] http://kwarc.info [2] http://www.jacobs-university.de [3] https://kwarc.info/projects/OAF 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. [4] http://opendreamkit.org/ 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. -- ---------------------------------------------------------------------- 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 m.kohlhase@jacobs-university.de http://kwarc.info/kohlhase ----------------------------------------------------------------------