_posts/2019-03-24-MMTVersion.md

+---
+layout: post
+author: dmueller
+title: "New MMT Version (16.0.0) Released"
+tags: 
+   - Announcements
+---
+A new [MMT Version (16.0.0)](https://github.com/UniFormal/MMT/releases/tag/v16.0.0) has been released.

_posts/2019-12-06-frederik.md

+---
+layout: post
+author: mkohlhase
+title: "Frederik Schaefer third best teaching assistant of the Technical Faculty at FAU"
+tags: 
+   - Announcements
+---
+KWARC's own Frederik Schaefer has been evaluated the third-best teaching assistant of the
+Technical Faculy ([Wahlfach 5-19 evaluations](https://www.apps.tf.fau.de/evaluation/ss19/index.html) for his work TAing [Artificial Intelligence II](http://kwarc.info/courses/ai2/). We are very proud of him. 
+

_posts/2019-12-16-slo.md

+---
+layout: post
+author: mkohlhase
+title: "KWARC wins bilateral DAAD travel grant with Slovenia"
+tags: 
+   - Announcements
+---
+[DAAD](http://daad.de) has awarded a two-year travel grant "MathDataHub" to KWARC and a research group around Primoz Potoci at the University of Ljubliana in Slovenia. We will use the money for collaboration on [DataMathHub](http://data.mathhub.info) and establishing Math Data Workshops. 
+

_posts/2020-05-15-FrameIT.md

+---
+layout: post
+author: rmarcus
+title: "Logic and Video Games: a Rework of FrameIT"
+tags: 
+   - Announcements
+---
+We have released the Unity based framework [UFrameIT](https://kwarc.info/systems/frameit/) as a major rework of the original FrameIT.
+A paper that describes this effort has been accepted to [CICM 2020](https://cicm-conference.org/2020/cicm.php).
+
+The FrameIT project builds a Framework for Serious Games by combining Virtual Worlds with Mathematical Knowledge Management.
+There are many starting points for further research and we would be happy to have more students join this project.
\ No newline at end of file

_posts/2021-12-01-VoLL-KI.md

+---
+layout: post
+author: mkohlhase
+title: KWARC leads BMBF project VoLL-KI (2021-2015)
+tags:
+  - Announcements
+  - Voll-KI 
+---
+Today, the KWARC group starts a new project: [VoLL-KI](https://voll-ki.de) (Von Lernenden
+Lernen: AI Methods for Tertiary education). This project is funded by BMBF with 5M€
+ - overall joint project with Uni Bamberg and Hochschule Coburg - 2M€ for FAU, split
+between the KWARC group and the [DDI group (Didactics of Computer Science](https://www.ddi.tf.fau.de/). 
+   
+[Prof. Kohlhase](https://kwarc.info/kohlhase) coordinates the [overall project](https://voll-ki.de). 

_posts/2022-02-01-welcome-timur.md

+---
+layout: post
+author: mkohlhase
+title: Welcome Timur Fayzrakhmanov (Proect VoLL-KI)
+tags:
+  - Announcements 
+---
+The [VoLL-KI](https://voll-ki.de) project welcomes a new member: Timur Fayzrakhmanov who
+joins us from Kazan. 

_posts/2022-02-10-HIM-trimester.md

+---
+layout: post
+author: mkohlhase
+title: "Special Trimester on \"Prospects of Formalized Mathematics\" at the Hausdorff Institute of Mathematics in Bonn"
+tags:
+  - Announcements
+---
+The [Hausdorff Institute of Mathematics](https://www.him.uni-bonn.de/) will offer a
+Special [Trimester on "Prospects of Formalized Mathematics"](https://www.him.uni-bonn.de/programs/future-programs/future-trimester-programs/prospects-of-formal-mathematics/description/) May-August 2024.
+[Prof. Kohlhase](https://kwarc.info/kohlhase) coordinates the organization. 

_posts/2022-02-27-sTeX3@CTAN.md

+---
+layout: post
+author: mkohlhase
+title: "sTeX3 Release on CTAN"
+tags:
+  - Announcements
+---
+[sTeX3](https://github.com/slatex/stex) is a complete rewrite of sTeX - An infrastructure
+for semantic preloading of LaTeX documents - in the LaTeX3 framework. It has just been
+released to [CTAN](https://ctan.org) the Comprehensive TeX Archive Network, and will be
+part of [TeXLive 2022](https://www.tug.org/texlive/) due out in April.  
+
+After almost 15 years, sTeX needed a complete makeover to regularize syntax, weed out
+unused and deprecated features, and synchronize it better with the
+[MMT](https://uniformal.github.io) system and functionality. 
+
+Compared to sTeX1, the new implementation does away with the need for external systems in
+the PDF workflow, allows to add sTeX functionality to arbitrary document classes, and
+completely reworks the XML-based content generation. Instead of using a
+[LaTeXML](https://math.nist.gov/~BMiller/LaTeXML/) fork we use
+[RusTeX](https://github.com/slatex/RusTeX/) a new TeX engine that directly interprets the
+sTeX3 packages and generates semantically annotated XHTML5 which can then be harvested by
+[MMT](https://uniformal.github.io) for further knowledge management services. 
+
+Further development of the sTeX ecosystem (the packages, an IDE, RusTeX, ...) will
+continue on [sLaTeX group on GitHub](https://githhub.com/sLaTeX).

_posts/2022-05-04-MMT-release-22.md

+---
+layout: post
+author: mkohlhase
+title: "MMT Release 22"
+tags:
+  - Announcements
+---
+After almost 18 months of development, [MMT](https://uniformal.github.io) - the flagship
+system of the KWARC group - has been released in [version
+22](https://github.com/UniFormal/MMT/releases/tag/v22.0.0).
+
+The long development time of this release has been a consequence of the growing
+inter-dependency of the system-near library and the system code, which led to serious
+maintenance problems in the past. Another problem was that a lot of dead code had
+accumulated over the last decade. 
+
+These problems have been addressed in version 22 (see the [release
+notes](https://github.com/UniFormal/MMT/releases/tag/v22.0.0) for details) and we hope
+that MMT can now serve as a much more stable basis for mathematical knowledge management
+and we can return to a faster release cycle for the future. 

_posts/2022-08-11-introducing-stex3.md

+---
+layout: post
+author: dmueller
+title: "Presenting sTeX3"
+tags:
+  - Announcements
+---
+[Dennis Müller](/people/dmueller)'s recent presentation on and demonstration of the [sTeX3](https://github.com/slatex/stex) system at the [TeX Users Group Conference 2022](https://tug.org/tug2022/) is now available on [YouTube](https://youtu.be/QXSO6IQ-SX4).

_posts/2022-09-14-tipes.md

+---
+layout: post
+author: frabe
+title: "Representing Scientific Knowledge"
+tags:
+  - Announcements
+---
+[Florian Rabe](https://kwarc.info/people/frabe/) gives [invited talk](https://kwarc.info/people/frabe/Research/slides/rabe_tipes_22.pdf) at the [annual meeting](https://indico.nbi.ku.dk/event/1784/) of the [TiPES project](https://www.tipes.dk/) on Tipping Points in the Earth System.

_posts/2022-09-23-europroofnet.md

+---
+layout: post
+author: frabe
+title: "Exporting Proof Assistant Libraries"
+tags:
+  - Announcements
+---
+[Florian Rabe](https://kwarc.info/people/frabe/) gives [invited talk](https://kwarc.info/people/frabe/Research/slides/rabe_oafexp_22.pdf) at [EuroProofNet workshop](https://cicm-conference.org/2022/cicm.php?event=euproofnet&menu=general) on the development, maintenance, refactoring and search of large libraries of proofs.

_posts/2022-10-24-dagstuhl.md

+---
+layout: post
+author: frabe
+title: "Automated mathematics: integrating proofs, algorithms and data"
+tags:
+  - Announcements
+---
+[Florian Rabe](https://kwarc.info/people/frabe/) will co-organize a [Dagstuhl Seminar](https://www.dagstuhl.de/seminars/seminar-calendar/seminar-details/23401) on automated mathematics in October 2023.

_posts/2023-01-20-lean_export.md

+---
+layout: post
+author: frabe
+title: "Lean Export in MMT"
+tags:
+  - Announcements
+---
+Starting with [the most recent devel commit](https://github.com/UniFormal/MMT/commit/1c79ed7edff9ddf3af63073adaf5f33031cd0267) MMT includes an export of the Lean prover libraries (via the low-level export files as parsed by the [treppline](https://github.com/gebner/trepplein) library.

_posts/2023-01-23-hcm.md

+---
+layout: post
+author: frabe
+title: "The Future of Formalized Mathematics"
+tags:
+  - Announcements
+---
+[Florian Rabe](https://kwarc.info/people/frabe/) gives [colloquium talk](https://kwarc.info/people/frabe/Research/slides/rabe_future_23.pdf) at the [Hausdorff Center of Mathematics](https://www.hcm.uni-bonn.de/hcm-home/) in Bonn.

contact.md

@@ -8,12 +8,12 @@ For general questions, contact the head of the group:
 
 *Professur für Wissensrepräsentation und -verarbeitung*; Informatik, FAU Erlangen-Nürnberg
 
-**Office**: Martensstraße 3, 91058 Erlangen, Room11.139, tel/fax: (49) 9131-85-64052/55, <michael.kohlhase@fau.de>
+**Office**: Martensstraße 3, 91058 Erlangen, Room11.139, tel/fax: (49) 9131-85-64052/55, michael.kohlhase  [at] fau.de
 
-**Secretary**: Gabriele Schönberger, Room 11.158, tel/fax: (49) 9131-85-64052/55, <gabriele.schoenberger@fau.de>
+**Secretary**: Gabriele Schönberger, Room 11.158, tel/fax: (49) 9131-85-64052/55, gabriele.schoenberger [at] fau.de
 
 For specific questions, please contact the members of the KWARC group directly or use the mailing lists:
 
- * <core@kwarc.info> (the core group, i.e. PIs, postdocs, and Ph.D. students)
- * <group@kwarc.info> (all KWARCies, i.e. including students)
- * <admin@kwarc.info> (for systems, ...)
+ * core [at] kwarc.info (the core group, i.e. PIs, postdocs, and Ph.D. students)
+ * group [at] kwarc.info (all KWARCies, i.e. including students)
+ * admin [at] kwarc.info (for systems, ...)

courses/AIProj.md

 ---
 layout: course
 
-title: Projekt zur Künstlichen Intelligenz
+title: AI Research Project
 instructors:
     - mkohlhase
-    - dmueller
+    - frabe
 semesters: 
-    - WS17/18
-    - SS17 
-    - WS16/17
     - SS16
+    - WS16/17
+    - SS17 
+    - WS17/18
+    - SS18 
+    - WS18/19
+    - SS19 
+    - WS19/20
+    - SS20 
+    - WS20/21
+    - SS21 
+    - WS21/22
+    - SS22 
 ---
 The KWARC group offers guided research projects in Artificial Intelligence either at the Bachelor's level or the Master's level.
-The topics of these projects are individually tailored to the student's interest and the projects themselves will be supervised closely by senior KWARC members. 
+The topics of these projects are individually tailored to the student's interest and the
+projects themselves will be supervised closely by senior KWARC members.
+
+Projects will consist of a research/development project commensurable in size with the
+ECTS points awarded, and end in a research report that documents it. 
+
+Even though administratively, AI Projects are tied to particular semesters, the research
+itself can be conducted at any time, and we are quite flexible in scheduling.  
 
-See the [KWARC research page](/research/) for a general introduction to the research and [the KWARC research topics list](http://gl.kwarc.info/kwarc/thesis-projects) for expemplary topics. 
+See the [KWARC research page](/research/) for a general introduction to the research
+conducted in the KWARC group and
+[the KWARC research topics list](http://gl.kwarc.info/kwarc/thesis-projects) for
+exemplary topics.

courses/KRMT.md

 ---
 layout: course
-title: Logik-Basierte Wissensrepräsentation für Mathematisch/Technisches Wissen
+title: Logic-Based Representation of Mathematical/Technical Knowledge
 instructors:
-    - mkohlhase
-    - dmueller
+  - mkohlhase
+  - frabe
 semesters:
     - SS17 
     - SS18 
+    - SS19 
+    - SS20 
+    - SS21 
+    - SS22 
+    - SS23 
+    - SS25 
 ---
 
-Dieser Kurs behandelt Grundlagen der Mathematik, Modulare Formalisierung in
-Theoriegraphen, Narrative Strukturen in informellen mathematisch/technischen Dokumenten,
-Formalisierung von Logiksprachen in Metalogiken.
+This course covers the foundations of mathematics, modular formalizations in theory graphs,
+narrative structures in informal mathematical/technical documents, and the formalization
+of logical languages in meta-logical frameworks. 
 
-Da wir nur wenige Studenten erwarten, wollen wir diesen Kurs sehr interaktiv und
-Projektorientiert aufbauen. Im wesentlichen werden wir gemeinsam mathematisches Wissen und
-Beschreibungssprachen in [OMDoc/MMT](http://uniformal.github.io) formalisieren.
+This is (tradictionally) a small course, so we can make it very interactive and
+project-like. The contents are split between 
+* lectures, where we discuss the concepts and
+* labs, where we jointly formalize mathematical knowledge and representation languages in
+  [OMDoc/MMT](http://uniformal.github.io).
 
-Materialien:
+Materials:
 
-* [Course Notes (Computational Logic)](http://kwarc.info/teaching/KRMT)
-* [Tutorial zur Formalisierung](https://gl.mathhub.info/Teaching/KRMT/blob/master/source/tutorial/mmt-math-tutorial.pdf)
-* [Formalisierungen des letzten Kurses](https://gl.mathhub.info/Teaching/KRMT/tree/master/source)
-
-Diskussionen finden auf dem
-[FSI Forum KRMT](https://fsi.cs.fau.de/forum/150-Logikbasierte-Wissensrepraesentation) statt. Dies ist
-eine wichtige Quelle von Rat und Tat. Wir bemühen uns, auf dem Forum präsent zu sein, und
-schnell auf Fragen zu antworten. Also das Forum abonnieren! 
+* [KRMT on StudOn](https://www.studon.fau.de/crs4499012.html)
+* [Course on zoom](Https://fau.zoom.us/j/65839665250)
+* [Videos on FAU.tv](Https://www.fau.tv/course/id/3065)
+* [Course Notes, Resources](http://kwarc.info/teaching/KRMT)
+* [Formalization Tutorialz](https://gl.mathhub.info/Tutorials/Mathematicians/blob/master/tutorial/mmt-math-tutorial.pdf)
+* [Formalizations of the last years](https://gl.mathhub.info/Teaching/KRMT/tree/master/source)
  

courses/ai1.md

 ---
 layout: course
 
-title: Künstliche Intelligenz I
+title: Artificial Intelligence I
 instructors:
     - mkohlhase
 
 semesters:
     - WS16/17
     - WS17/18
+    - WS18/19
+    - WS19/20 
+    - WS20/21 
+    - WS21/22 
+    - WS22/23 
+    - WS23/24
+    - WS24/25 
 ---
 
+This course is the first part of a two-semester introduction into the field of Artificial
+Intelligence (AI). It introduces the foundations of symbolic AI, in particular: 
+
+* Agent Models as foundation of AI
+* Logic Programming in Prolog
+* Heuristic Search as a methdod for problem solving
+* Adversarial Search (automating board games) via heuristic search
+* Constraint Propagation
+* Logical Languages for knowledge representation
+* Inference and automated theorem proving
+* Classical Planning
+* Planning and Acting in the real world. 
+
+The course follows the book
+[Artificial Intelligence: A Modern Approach](https://www.pearson.com/us/higher-education/program/Russell-Artificial-Intelligence-A-Modern-Approach-3rd-Edition/PGM156683.html)
+by Stuart Russell und Peter Norvig. We use the third edition. 
+
+The course materials (e.g. [Course Notes](http://kwarc.info/teaching/AI/notes.pdf) or
+[Assignments](http://kwarc.info/teaching/AI/assignments.pdf), but also old exams and
+(some) solutions) are [here](http://kwarc.info/teaching/AI/). 
+
+The course forum on [StudOn](https://studon.fau.de) is an important source for advice and
+discussions. The instrutor and tutors try to be present to help. 
+
+### German Version (possibly out of date)
+
 Diese Vorlesung ist der erste Teil einer zwei-semestrigen Einführung in die Künstlichen
 Intelligenz (KI). Sie beschäftigt sich mit den Grundlagen der symbolischen KI,
 insbesondere
 
 * Agentenmodelle als  Grundlagen der KI
+* Logisches Programmieren in Prolog
 * Heuristische Suche als Methode zum Problemlösen
-* Constraint-Propagierung
+* Adversarielle Suche (Strategiespiele)
+* Probleme unter Rand- oder Nebenbedingungen (Constraint Propagation)
 * Logische Sprachen zur Wissensrepräsentation,
-* Inferenz
-* Automatisches Planen
+* Inferenz und Logisches Programmieren
+* Klassisches Planen
+* Planen und Agieren in der realen Welt
 
 Die Vorlesung folgt dem Buch
 [Artificial Intelligence: A Modern Approach](https://www.pearson.com/us/higher-education/program/Russell-Artificial-Intelligence-A-Modern-Approach-3rd-Edition/PGM156683.html)
@@ -30,6 +66,6 @@ Die Kursmaterialien (z.B. [Course Notes](http://kwarc.info/teaching/AI/notes.pdf
 finden sich in [hier](http://kwarc.info/teaching/AI/). 
 
 Diskussionen finden auf dem
-[FSI Forum KI-I](https://fsi.cs.fau.de/forum/144-Kuenstliche-Intelligenz) statt. Dies ist
+[StudOn](https://studon.fau.de) statt. Dies ist
 eine wichtige Quelle von Rat und Tat. Wir bemühen uns, auf dem Forum präsent zu sein, und
 schnell auf Fragen zu antworten. Also das Forum abonnieren! 

courses/ai2.md

 ---
 layout: course
 
-title: Künstliche Intelligenz II
+title: Artificial Intelligence II
 instructors:
     - mkohlhase
 
 semesters:
     - SS17 
     - SS18 
+    - SS19 
+    - SS20 
+    - SS21 
+    - SS22 
+    - SS23 
+    - SS24 
 ---
 
+This course is the second part of a two-semester introduction into the field of Artificial
+Intelligence (AI). It introducers the foundations of inference under uncertainty, machine
+learning and language understanding. The course builds on and continues the course 
+[Artificial Intelligence I](/courses/ai1/) from the winter semester. In particular, the course 
+covers
+
+* Inference under Uncertainty
+* Bayesian Networks
+* Rational Decision Theory (MDPs and POMDPs)
+* Machine Learning and Neural Networks
+* Natural Language Processing
+
+The course follows the book
+[Artificial Intelligence: A Modern Approach](https://www.pearson.com/us/higher-education/program/Russell-Artificial-Intelligence-A-Modern-Approach-3rd-Edition/PGM156683.html)
+by Stuart Russell und Peter Norvig. We use the third edition. 
+
+The course materials (e.g. [Course Notes](http://kwarc.info/teaching/AI/notes.pdf) or
+[Assignments](http://kwarc.info/teaching/AI/assignments.pdf), but also old exams and
+(some) solutions) are [here](http://kwarc.info/teaching/AI/). 
+
+The course forum on [StudOn](https://studon.fau.de) is an important source for advice and
+discussions. The instrutor and tutors try to be present to help. 
+
+### German Version (possibly out of date)
+
 Diese Vorlesung ist der zweite Teil einer zwei-semestrigen Einführung in die Künstlichen
 Intelligenz (KI). Sie beschäftigt sich mit den Grundlagen des Schliessens unter
 Unsicherheit, des maschinellen Lernens und des Sprachverstehens.  Der Kurs baut auf der