swuv.md

---
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
---

##### Das Seminar finded wie gewohnt statt, nur halt online

Dieses Seminar behandelt ausgewählte Themen aus dem Gebiet der Wissensrepräsentation und
-Verarbeitung, mit einem Fokus auf mathematischem Wissen.

Die Vortragsthemen sind sehr unterschiedlich im Schwierigkeitsgrad, sie reichen von
Einführungsthemen für ambitionierte Bachelor-Studenten bis zur Forschungsfront für
Doktoranden. Sie spiegeln recht gut die Forschungsinteressen der
[KWARC Gruppe](http://kwarc.info) wieder. Daher ist dieses Seminar sehr gut geeignet um in
die Arbeitsgruppe einzusteigen (z.B. für eine Master-Arbeit oder Promotion). 

*Seminartermin/Ort*: Donnerstag 14:15-15:45, in:
* zoom meeting room <https://fau.zoom.us/j/93424820605?pwd=d3N0M3pkVDBKclBnN3NzVnYwY3hGUT09>
* meeting ID: 934 2482 0605
* password: 027214

<!-- Raum 00.131-128, Cauerstraße 11 -->

|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

##### Vortragsthemen

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||
| Argumentation Logics | various topics||
| 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: 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)|Sondertermin|
| \*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
 -->