Newer
Older
---
layout: course
title: Seminar Wissensrepräsentation und -verarbeitung
instructors:
- mkohlhase
- frabe
semesters:
- SS17
- WS17/18
- SS18
- WS18/19
- SS19
- WS19/20
- SS20
- WS20/21
- SS21
##### Administrative
The seminar takes place every semester on Thursdays 14:15-15:45 throughout the lecture period.
It takes place in Room 00.131-128, Cauerstraße 11.
The seminar takes place in-person unless mentioned otherwise.
If we need to do it via zoom, we will use the following room:
* zoom meeting room <https://fau.zoom.us/j/93424820605?pwd=d3N0M3pkVDBKclBnN3NzVnYwY3hGUT09>
* meeting ID: 934 2482 0605
* password: 027214
##### Content and Audience
This seminar discusses selected topics from knowledge representation.
This is a wide field that pervades all of computer science and many adjacent sciences like mathematics and physics.
Typical topics involve
* formal languages (logics, programming languages, data description languages, ontologies, informal scientific languages, ...)
* tools for working with and applying such languages, both in general and domain-specific ones
* libraries of formal knowledge and systems for building, maintaining, and managing them
* knowledge-based services like search or user interfaces
In particular, the primary application of our research is mathematical knowledge, but we are always interested in other areas on a case-by-case basis.
The difficulty of topics varies from introductory topics for ambitious Bachelor students to research topics of PhD students.
We also occasionally have advanced talk from visiting researchers.
The social center of the seminar is the [KWARC research group](http://kwarc.info), and the talks reflect the current research in the group.
Therefore, the seminar is well-suited for newcomers, e.g., students interested in a Master thesis or PhD.
**Correction**: Some dates below were off-by-1 and have been corrected. The seminar will take place on **Thursdays**.
| 19. 10. 2022 | Kohlhase, Rabe | Admin, discussion of topics |
| 26. 10. 2022 | Kohlhase, Rabe | How to give a talk? |
| 03. 11. 2022 | Marcel Dreier | Extension of the MMT knowledge base for volume-based mathemantics questions in UFrameIT| MSc project presentation
| 10. 11. 2022 |
| 17. 11. 2022 |
| 24. 11. 2022 |
| 01. 12. 2022 |
| 08. 12. 2022 |
| 15. 12. 2022 |
| 22. 12. 2022 |
| 12. 01. 2023 |
| 19. 01. 2023 |
| 26. 01. 2023 |
| 02. 02. 2023 |
| 07. 02. 2023 |
Themen werden mit dem Dozenten individuell ausgemacht, typischerweise in den ersten Seminarterminen.
Vorschläge von Studenten sind möglich.
Zur groben Orientierung ist hier eine repräsentative Auswahl von nicht belegten Themen der letzten Jahre:
|Thema | Literatur | Schwierigkeitsgrad | vergeben? | Termin|
|-----|-------|-----|-------|---------|
| Distributed Ontology Language || Semantic Web needs Theory Graphs||
| Weak Type Theory|[[1]](http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/kjour.pdf)|relativ einfach, aber Logik-lastig| | |
| MathLang| Kamareddine | | |
| Formula Parsing | Ginev M.Sc., Pichler MSc., various AITP papers | relativ einfach | |
| Knowledger Representation/AI for Hanabi | google | medium | |
| Functional programming with bananas, lenses, envelopes and barbed wire| [[1]](https://research.utwente.nl/files/6142047/db-utwente-40501F46.pdf)|functional programming|
| MitM Foundation | | medium | | |
| LF + Intersection Types | | advanced| |
| McAllister-Foundation || with Voldemort's Theorem (difficult) |||
Diskussionen und finden auf dem [FSI Forum WuV](https://fsi.cs.fau.de/forum/151-Seminar-Wissensrepraesentation-und-verarbeitung)
statt. Dies ist eine wichtige Quelle von Ankündigungen sowie Rat und Tat. Wir bemühen uns,
auf dem Forum präsent zu sein, und schnell auf Fragen zu antworten. Also das Forum
abonnieren!
##### For the record: SS 2022
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 28. 04. 2022 | cancelled | |
| 05. 05. 2022 | Kohlhase, Rabe | Admin, discussion of topics |
| 12. 05. 2022 | cancelled |
| 19. 05. 2022 | Kohlhase, Rabe | How to give a talk? |
| 26. 05. 2022 | holiday| |
| 02. 06. 2022 | Kwarc group | Math Archives | group discussion
| 09. 06. 2022 | Luca Wolff | Automated Theorem Proving for MMT | BSc thesis presentation
| 16. 06. 2022 | holiday | |
| 23. 06. 2022 | moved to July 4 |
| 27. 06. 2022 | Takuto Asakura | Grounding Mathematical Identifiers | invited talk by visiting researcher
| 04. 07. 2022 | Katja Bercic | Mathematical Data | invited talk by visiting researcher
| 07. 07. 2022 | Sven Wille | Interactive Theorem Proving in MMT | MSc thesis presentation
| 14. 07. 2022 | Moritz Blöcher | Towards Functional Programming in LATIN2 | BSc thesis presentation
| 21. 07. 2022 | Navid Roux | A Framework for Diagram Operators | MSc thesis presentation: [slides](https://gl.kwarc.info/supervision/seminar/-/tree/master/SS2022/diagops/build/slides.pdf), [thesis](https://gl.kwarc.info/supervision/MSc-archive/-/blob/master/2022/RouxNavid.pdf)
| 28. 07. 2022 | Tobias Völk, Philip Kaludercic | Designing a Text Protocol for the Game of Kalah | joint seminar presentation
##### For the record: WS 2021/2022
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 21. 10. 2021 | Kohlhase, Rabe | Admin, Themenvergabe |
| 28. 10. 2021 | Annika Schmidt | Modular Formalization of Set Theory | MSc thesis presentation
| 04. 11. 2021 | Moritz Blöcher | Derived Inference Rules in LATIN | BSc project presentation
| 11. 11. 2021 | John Schihada | Knowledge-Based Physics Simulation| MSc thesis presentation
| 18. 11. 2021 | Alexander Steen | Introduction Automated Reasoning | Juridicum, parallel event
| 25. 11. 2021 | cancelled | |
| 02. 12. 2021 | Dennis Müller | Combining Statistical Machine Learning and Inductive Logic Programming | a general talk inspired by his 6 month visit at Fraunhofer Institute for Integrated Circuits
| 09. 12. 2021 | Max Rapp | Formalizing Argumentation Logics | PhD thesis progress talk
| moved to 5pm, 20. 12. 2021 | Ivo Junior | Interfacing Mathematical Human-Computer Interactions by Using the Grammatical Logical Inference Framework | BSc. Presentation |
| 23. 12. 2021 | cancelled | |
| 06. 01. 2022 | cancelled | |
| 13. 01. 2022 | Fabian Brinkmann | Algebraic Language Theory |
| 20. 01. 2022 | Tim Friederich| A Semantic Search Engine for Quality Management | BSc thesis presentation
| 27. 01. 2022 | cancelled | |
| 03. 02. 2022 | Names in DRT | Michael Kohlhase |
| 10. 02. 2022 | Chase Ford | Coalgebra | part of collaboration with Inf 8 group
##### For the record: Seminarplan SS21
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 14. 04. 2021 | Rabe | Admin, Themenvergabe |
| 21. 04. 2021 14:45-16:15 | Sven Wille | Towards an interactive proof system for MMT | MSc. proj. presentation
| 29. 04. 2021 | cancelled | |
| 06. 05. 2021 |Kohlhase, Rabe | How to give a talk?|
| 13. 05. 2021 | holiday | |
| 20. 05. 2021 |Kohlhase, Rabe | How to read a paper?|
| 27. 05. 2021 | Rabe | Type-Dependent Equality | practice talk for CICM
| 03. 06. 2021 | holiday | |
| 10. 06. 2021 | Wagner, Rabe | OEIS in MMT | guided discussion of open problem
| 17. 06. 2021 | Rabe (moderator) | Big Math and the One-Brain Barrier | reading group
| 24. 06. 2021 | Jonas Betzendahl | Formalising and Proving with Sudokus |
| 01. 07. 2021 | Navid Roux | [Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style](https://kwarc.info/people/frabe/Research/RR_softening_21.pdf) | practice talk for LFMTP
| 08. 07. 2021 | Roman Hucke | DOL and OntoHub | seminar talk
| 15. 07. 2021 | Johannes Westphal | GLIF | seminar talk
##### For the record: Seminarplan WS2021
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 04. 11. 2020 | Rabe | Admin, Themenvergabe |
| 11. 11. 2020 | Kohlhase, Rabe | How to read a scientific paper? |
| 18. 11. 2020 | Kohlhase, Rabe | How to give a scientific talk? |
| 25. 11. 2020 | | entfällt |
| 02. 12. 2020 | Jonas Betzendahl | Formalizing Undefinedness: A survey |
| 09. 12. 2020 | Michael Banken | Theory Intersection| Msc. thesis presentation
| 16. 12. 2020 | Jan Frederik Schaefer | Prototyping NLU Pipelines -- A Type-Theoretical Framework | Msc. thesis presentation ([slides](https://github.com/jfschaefer/slides/raw/master/2020/swuv-msc-presentation/slides.pdf), [thesis](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2020/Schaefer_Jan_Frederik.pdf))
| 23. 12. 2020 | entfällt | |
| 13. 01. 2021 | Christian Cerny | Term Generation in MMT | BSc. thesis presentation
| 20. 01. 2021 | Markus Wich | Autoformalization of Mathematics | [slides](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/wich-slides.pdf), [manuscript](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/wich.pdf)
| 27. 01. 2021 | Navid Roux | A Beginner's Guide to Logical Relations for a Logical Framework | [slides](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/logrels/slides.pdf), [manuscript](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/logrels/guide.pdf), [underlying paper](https://kwarc.info/people/frabe/Research/RS_logrels_12.pdf)
| 03. 02. 2021 | Sebastian Weber | The UFrameIT Project | [manuscript](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/weber.pdf)
| 10. 02. 2021 | Max Rapp | Sequent Calculi for Argumentation and/or Adaptive Logics|
##### For the record: Seminarplan SS20
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 22. 04. 2020 | Rabe | Admin, Themenvergabe |
| 22. 04. 2020 | Navid Roux | Functorial Diagram Operators |
| 29. 04. 2020 | Kohlhase| Themenvergabe, Workshop-Vortrag|
| 06. 05. 2020 | ---- | fällt aus|
| 13. 05. 2020 | Benjamin Bösl| FrameIT: A Logic-Based Framework for Serious Games |
| 20. 05. 2020 | Tom Wiesing | Interactions between aspects of Tetrapodal Mathematics on MathHub | [Slides](https://kwarc.info/people/twiesing/pubs/slides/2020_05_20_phdproposal.pdf) |
| 27. 05. 2020 | Dennis Müller | From Informal to Formal Mathematics |
| 03. 06. 2020 | Benjamin Gorny | Knowledge Representation in DeepMind|
| 10. 06. 2020 | entfällt| |
| 17. 06. 2020 | entfällt| |
| 24. 06. 2020 | Jan Frederik Schaefer | ELPI and MMT |
| 01. 07. 2020 | Jan Frederik Schaefer | GLIF/Jupyter|
| 08. 07. 2020 | entfällt| |
| 15. 07. 2020 | Annika Schmidt | Curry Howard Isomorphism|
| 22. 07. 2020 | Pascal Zoleko | A Symbolic Approach to Job Recommendation.|
| 29. 07. 2020 | Florian Stangl | Something about Jupyther |
##### For the record: Seminarplan WS19/20
|Datum|Sprecher|Thema|Notiz|
|-----|--------|-----|----|
| 16. 10. 2019 | Rabe | Admin, Themenvergabe |
| 23. 10. 2019 | Michael Kohlhase| How to read scientific articles|
| 30. 10. 2019 | - | no seminar |
| 6. 11. 2019 | Rabe/Kohlhase | How to give a talk|
| 13. 11. 2019 | Max Rapp |Formalising the Law in Theory Graphs |
| 20. 11. 2019 | Florian Rabe | Intermediate Language for Formalization|
| 27. 11. 2019 | Florian Rabe | Category of Theories, Diagram Operators |
| 4. 12. 2019 | Katja Berčič | Research data in mathematics: taking the high road |
| 11. 12. 2019 | --- | no seminar|
| 18. 12. 2019 | Christoph Alt | Formula Search for the nLab|
| 8. 1. 2020 | --- | no seminar |
| 15. 1. 2020 | Takuto Asakura (NII Tokyo) | Towards Grounding of Formulae in Mathematical Objects|
| 22. 1. 2020 | Navid Roux | Composition of Programming Languages |
| 29. 1. 2020 | -- | no seminar |
| 5. 2. 2020 | -- | no seminar|
##### For the record: Seminarplan SS2019
|Datum|Sprecher|Thema|Notiz|
|-----|-------|-----|-----|
| 24.4. 2019| Rabe | Admin, Themenvergabe ||
| 1. 5. 2019 | - | Maifeiertag ||
| 8. 5. 2019 | Richard Marcus | 3D Visualization of Theory Graphs||
| 15. 5. 2019 | Michael Torpey (St. Andrews) | Persistent Memoization between Computer Algebra Systems||
| 22. 5. 2019 | - | entfaellt||
| 29. 5. 2019 | - | Christi Himmelfahrt||
| 5. 6. 2019 | Marcel Rupprecht | Visualization of Theory Graphs ||
| 12. 6. 2019| Frederik Schaefer | GF + MMT = GLF - From Language to Semantics Through LF||
| 19. 6. 2019 | - | entfaellt ||
| 26. 6. 2019 | Tom Wiesing | Integrating semantic mathematical documents and dynamic notebooks||
| 3. 7. 2019 | Jonas Beyer | Morphoid Type Theory||
| 10. 7. 2019 | - | entfaellt ||
| \*15. 7. 2019, 14:00 | Navid Roux | Refactoring Theory Graphs in KM Systems (Raum 11.139) | BSc thesis presentation: [slides](https://gl.kwarc.info/supervision/seminar/-/tree/master/SS2019/refactoring-theory-graphs/build/slides.pdf), [thesis](https://gl.kwarc.info/supervision/BSc-archive/-/blob/master/2019/Roux_Navid.pdf) |
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
| \*17. 7. 2019 | Kathrin Horsting| Somthing with WissKI|Cauerstraße 4, Raum 0.332|
| 24. 7. 2019 | - | entfaellt ||
##### For the record: Seminarplan SS2018
|Datum|Sprecher|Thema|
|-----|-------|-----|
| 11. 4. 2018| Michael Kohlhase| Admin, Themenvergabe | -- |
| 18.4. 2018 | Entfällt| |
| 25. 4. 2018 | Michael Kohlhase| How to read scientific articles|
| 2. 5. 2018 | Entfällt ||
| 9. 5. 2018 | Michael Kohlhase | ALMANAC: Argumentation Logics Manager & Argument Context Graph|
| 16. 5. 2018 | Entfällt| | |
| 23. 5. 2018 | Dennis Müller| Records as Types |
| 30. 5. 2018 | Entfällt| | |
| 6. 6. 2018 | Frederik Schaefer| Math in GF|
| 13. 6. 2018 | Makarius Wenzel (Augsburg) | Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents |
| 20. 6. 2018 | Entfällt| | |
| 27. 6. 2018 | Alpcan Dalga | OpenMath & SCSCP |
| 4. 7. 2018 | Martin Holzwarth | Framing |
| 11. 7. 2018 | Jonny Schäfer | <Something with Argumentation>|
##### For the record: Seminarplan WS2017/18
|Datum|Sprecher|Thema|
|-----|-------|-----|
| 25. 10. 2017| Michael Kohlhase| How to read scientific articles|
| 1. 11. 2017 | Allerheiligen | ------ |
| 8. 11. 2017| Tom Wiesing| Virtual Theories as a Uniform Interface to Mathematical Data Sources|
| 15. 11. 2017 | Michael Kohlhase| Knowledge-Based Interoperability for Mathematical Software Systems|
| 22. 11. 2017 | ----- | ----- |
| 29. 11. 2017| Theresa Pollinger|Model Knowledge Representation for HPC|
| 6. 12. 2017 | ----- | ----- |
| 13. 12. 2017 | ----- | ----- |
| 20. 12. 2017 | Michael Kohlhase | Visual structure in math vexpressions. |
| 10. 1. 2018 | Florian Rabe | String Interpolation in MMT |
| 24. 1. 2018 | Frederik Schäfer| Weak Type Theory|
| 31. 1. 2018| ---- | ------|
<!-- LocalWords: mkohlhase Logik-lastig Kamareddine Ginev MitM-based Interection
-->