events/GILogicWorkshops/2022/cfp.txt

+Joint Logic Workshop: Logic in Computer Science and Deduction Systems
+– 26. Jahrestagung FG LogInf und Workshop der FG DedSys –
+https://kwarc.info/events/GILogicWorkshops/index.html
+
+Online Workshop hosted by FAU University Erlangen-Nürnberg
+Friday, April 8, 2022, whole day event
+
+==========================
+= CALL FOR CONTRIBUTIONS =
+==========================
+
+== Overview ==
+
+The annual Workshop on Logic in Computer Science (Jahrestagung)
+is the prime activity of the Interest Group on Logic in Computer Science (FG LogInf)
+of the German Society of Informatics (Gesellschaft für Informatik, GI).
+Together with the Interest Group on Deduction Systems (FG DedSys) of the GI
+the Joint Logic Workshop fosters mutual exchange and aims at exploring synergies
+between both groups.
+
+The Joint Logic Workshop is a meeting with an informal and friendly atmosphere,
+where everyone (not only the German community) interested in the relevant topics
+can report on their work in an accessible setting.
+
+A special focus of the workshop is on young researchers and students,
+who are particularly encouraged to present their ongoing research
+projects to a wider audience. Another goal of the meeting is to stimulate
+networking effects and to foster collaborative research projects.
+
+Because of the ongoing pandemic situation the Joint Logic Workshop is organized
+as an online event. Organizational details are published on the event's website.
+
+
+== Invited speakers ==
+
+We plan to have 1-2 invited talks; details will follow soon.
+
+
+== Organization ==
+
+We welcome contributions on all theoretical, experimental and applied
+aspects of formal logic, reasoning and deduction.
+Accepted contributions are presented in a talk of approx. 15-30 minutes
+(depending on the overall number of accepted contributions), including
+discussion.
+
+The Joint Logic Workshop will also host the annual general assembly
+(Mitgliederversammlungen) of FG LogInf.
+
+The Joint Logic Workshop is kindly hosted by the Theoretical Computer Science
+and Knowledge Representation groups at University of Erlangen-Nürnberg (FAU)
+and organized by Sergey Goncharov and Florian Rabe.
+
+
+== Submission ==
+
+Submission is open to everybody interested in logic and/or deduction systems.
+
+Please submit an extended abstract (max. one page) of your contribution to
+both Olaf Beyersdorff <olaf.beyersdorff@uni-jena.de> and 
+Alexander Steen <alexander.steen@uni-greifswald.de.
+Submissions will be weakly reviewed to ensure topical fit.
+
+Submission deadline: March 21, 2022
+Notification:        March 25, 2022
+
+
+== Scientific Committee ==
+
+Olaf Beyersdorff, University of Jena
+Thomas Schneider, University of Bremen
+Claudia Schon, University of Koblenz
+Alexander Steen, University of Greifswald
+

events/GILogicWorkshops/2022/cfpart.txt

+Joint Logic Workshop: Logic in Computer Science and Deduction Systems
+– 26. Jahrestagung FG LogInf und 33. Jahrestreffen FG DedSys (Deduktionstreffen) –
+https://kwarc.info/events/GI2020/index.html
+
+Online Workshop hosted by FAU University Erlangen-Nürnberg
+Friday, March 26, 2021, whole day event
+
+==========================
+= CALL FOR PARTICIPATION =
+==========================
+
+== Overview ==
+
+The annual Workshop on Logic in Computer Science (Jahrestagung)
+and the annual meeting Deduktionstreffen are the prime activities of the
+Interest Group on Logic in Computer Science (FG LogInf) and the
+Interest Group on Deduction Systems (FG DedSys) of the
+German Society of Informatics (Gesellschaft für Informatik), respectively.
+This year, the activities will be organized as a Joint Logic Workshop in order
+to foster mutual exchange and to explore potential synergies.
+
+The Joint Logic Workshop is a meeting with an informal and friendly atmosphere,
+where everyone (not only the German community) interested in the relevant topics
+can report on their work in an accessible setting.
+
+Because of the ongoing pandemic situation the Joint Loic Workshop had to be cancelled
+in 2020 and is now organized as an online event.
+Organizational details are published on the event's website.
+
+== Program ==
+
+The workshop will feature invited talks by Ana Sokolova and Dov Gabbay and 11 contributed talks.
+
+The detailed program is available at https://kwarc.info/events/GI2020/index.html
+
+The Joint Logic Workshop will also host the annual general assemblies
+(Mitgliederversammlungen) of both special interest groups.
+
+== Registration ==
+
+Participation is free, but an informal registration is necessary at https://docs.google.com/forms/d/1hF5TgGreilNI6YYEI7b1PbMYNnmxqIgnSKWN6JMOJko
+
+== Scientific Committee ==
+
+Olaf Beyersdorff, University of Jena
+Thomas Schneider, University of Bremen
+Claudia Schon, University of Koblenz
+Alexander Steen, University of Luxembourg
+
+The Joint Logic Workshop is kindly hosted by the Theoretical Computer Science
+and Knowledge Representation groups at University of Erlangen-Nürnberg (FAU)
+and organized by Sergey Goncharov and Florian Rabe.

events/GILogicWorkshops/index.md

+---
+layout: page
+title: GI Meeting Deduction and Logic
+---
+
+The 2020-2022 annual meetings of the GI groups [Deduction Systems](https://fg-dedsys.gi.de/) and [Logic in Computer Science](https://fg-loginf.gi.de/)
+(Gemeinsames Jahrestreffen der GI-Fachgruppen Deduktionssysteme und Logik in der Informatik) take place jointly in Erlangen.
+They are organized by [Sergey Goncharov](https://www8.cs.fau.de/sergey) and [Florian Rabe](https://kwarc.info/people/frabe/).
+
+In fact, due to COVID-19 pandemic, online meetings took place.
+An in-person meeting of Deduction Systems is planned for 2022 as a part of the KI conference.
+
+The 2021 meeting is [here](2021/index.html).
+
+### Program of the Spring 2022 Meeting
+
+The meeting will take place online on April 8.
+The call for contributions is [here](2022/cfp.txt).
+
+The program will consist of multiple sessions of zoom talks in the zoom room https://fau.zoom.us/j/63889416032.
+The program is as follows:
+
+* Session 1: 10:00 - 11:00 (chair: Claudia Schon)
+  * 10:00: Martin Suda, **Invited talk** Integrating Machine Learning into Saturation-based ATPs [slides (if any)](2022/suda.pdf)
+* Break 1: 11:00 - 11:30: free discussion in zoom
+* Session 2: 11:30 - 13:00 (chair: Florian Rabe)
+  * 11:30: Florian Wörz, Number of Variables for Graph Differentiation and the Resolution of GI Formulas [slides (if any)](2022/woerz.pdf)
+  * 12:00: Martin Lange, The Calculus of Influence - Formal Modelling of Biological Experiments [slides (if any)](2022/lange.pdf)
+  * 12:30: Florian Bruse, Model Checking Timed Recursive CTL, [slides (if any)](2022/bruse.pdf)
+* Lunch break: 13:00 - 14:00
+* Session 3: 14:00 - 15:30 (chair: Sergey Goncharov)
+  * 14:00: Colin Rothgang, Theorem Proving in Dependently Typed Higher-Order Logic [slides (if any)](2022/rothgang.pdf) 
+  * 14:30: Jean Christoph Jung and Frank Wolter, Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments [slides (if any)](2022/jung.pdf)
+  * 15:00: Hendrik Leidinger, SCL for First-Order Logic with Equality,  [slides (if any)](2022/lange.pdf)
+* Break 2: 15:30 - 16:00: free discussion in zoom
+* Session 4: 16:00 - 17:00 (chair: Olaf Beyersdorff)
+  * 16:00: Marijn Heule, **Invited talk** Short Proofs in Strong Proof Systems Fragments [slides (if any)](2022/heule.pdf)
+* Session 5: 17:15 - 18:00: Mitgliederversammlung Fachgruppe LogInf

events/Tetrapod-2018.md

----
-layout: page
-title: Modular Knowledge
----
-<p style="text-align:center;font-weight:bold" markdown="1">
-Workshop on Modular Knowledge (Tetrapod)<br/>
-Oxford, July 13, 2018<br/>
-at the [Federated Logic Conference 2018](http://www.floc2018.org/)<br/>
-affiliated with the [Third International Conference on Formal Structures for Computation and Deduction](http://www.cs.le.ac.uk/events/fscd2018/)
-</p>
-
-#### Description
-
-Mathematics, logics, and computer science support a rich ecosystem of formal knowledge.
-  This involves many interrelated human activities such as modeling phenomena and formulating conjectures, proofs, and computations, and organizing, interconnecting, visualizing, and applying this knowledge.
-  To handle the ever increasing body of knowledge, practitioners employ a rapidly expanding set of representation languages and computer-based tools centered around the four fundamental paradigms of formal deduction, computation, datasets, and informal narration.
-
-Modularity has been recognized in all FLoC-related communities as a critical method for designing scalable representation languages and building large corpora of knowledge.
-  It is also extremely valuable for comparing and exchanging knowledge across communities, corpora, and tools - a challenge that is both pressing and difficult.
-
-Expanding on the Tetrapod workshop at the conference on intelligent computer mathematics (CICM) 2016, this workshop brings together researchers from a diverse set of research areas in order to create a universal understanding of the challenges and solutions regarding highly structured knowledge bases.
-
-Of particular interest are
-* foundational principles such as theory graphs and colimits
-* interchange languages and module systems
-* languages and tools for representing, reasoning, computing, managing, and documenting modular knowledge bases
-
-#### Format
-
-- There will be 6 invited speakers, each of which will be asked to present a specific topic.
-- Each speaker will give a 15-minute presentation on that topic that is followed by a 
-     30-minute discussion session.
-- There will not be a call for papers or other contributions.
-     However, there will be a call for participation that will include the invited speakers and their topics.
-
-#### Invited speakers and topics
-
-| Speaker           | Modularity in...         |
-| ----------------- | ------------------------ |
-| Catherine Dubois  | Proof Checking           |
-| Georges Gonthier  | Large Proofs             |
-| Till Mossakowski  | Ontologies               |
-| Natarajan Shankar | Proof Assistants         |
-| Doug Smith        | Software Synthesis       |
-| Nicolas M. Thiery | Mathematical Computation |
-
-#### Call for Opinions
-
-To improve the discussions, we invite all interested researchers (independent of whether they attend the workshop) to submit preformulated opinions, either on one of the 6 subtopics or on modularity in general.
-
-Opinions include any valuable contribution to the discussion such as
-* position statements
-* strengths and weaknesses of existing solutions
-* pointers to pertinent recent or ongoing work
-* challenge and benchmark problems
-
-Opinions should be brief enough that workshop participants can easily read all opinions at the beginning of each session.
-Typically, they will not be longer than a couple of paragraphs.
-
-The organizers will curate the submitted opinions and publish them on the workshop website and in a post-workshop summary.
-
-For the version circulated at the workshop, the organizers may (with the collaboration of the authors) summarize or merge individual opinions if that helps readability. The online version will list all opinions verbatim.
-Opinions will be listed together with the name(s) of the authors.
-
-Opinions should be submitted at https://easychair.org/conferences/?conf=tetrapod18 (An easychair abstract without a pdf file is sufficient.)
-
-#### Organizers
-
-- Jacques Carette, McMaster University (carette@mcmaster.ca)
-- Dennis Müller, FAU Erlangen-Nürnberg (d.mueller@kwarc.info)
-- Florian Rabe, Jacobs University Bremen (f.rabe@jacobs-university.de)

events/Tetrapod2018/index.md

+---
+layout: page
+title: Modular Knowledge
+---
+<p style="text-align:center;font-weight:bold" markdown="1">
+Workshop on Modular Knowledge (Tetrapod)<br/>
+Oxford, July 13, 2018<br/>
+at the [Federated Logic Conference 2018](http://www.floc2018.org/)<br/>
+affiliated with the [Third International Conference on Formal Structures for Computation and Deduction](http://www.cs.le.ac.uk/events/fscd2018/)
+</p>
+
+#### Description
+
+Mathematics, logics, and computer science support a rich ecosystem of formal knowledge.
+  This involves many interrelated human activities such as modeling phenomena and formulating conjectures, proofs, and computations, and organizing, interconnecting, visualizing, and applying this knowledge.
+  To handle the ever increasing body of knowledge, practitioners employ a rapidly expanding set of representation languages and computer-based tools centered around the four fundamental paradigms of formal deduction, computation, datasets, and informal narration.
+
+Modularity has been recognized in all FLoC-related communities as a critical method for designing scalable representation languages and building large corpora of knowledge.
+  It is also extremely valuable for comparing and exchanging knowledge across communities, corpora, and tools - a challenge that is both pressing and difficult.
+
+Expanding on the Tetrapod workshop at the conference on intelligent computer mathematics (CICM) 2016, this workshop brings together researchers from a diverse set of research areas in order to create a universal understanding of the challenges and solutions regarding highly structured knowledge bases.
+
+Of particular interest are
+* foundational principles such as theory graphs and colimits
+* interchange languages and module systems
+* languages and tools for representing, reasoning, computing, managing, and documenting modular knowledge bases
+
+#### Format
+
+- There will be 6 invited speakers, each of which will be asked to present a specific topic.
+- Each speaker will give a 15-minute presentation on that topic that is followed by a 
+     30-minute discussion session.
+- There will not be a call for papers or other contributions.
+     However, there will be a call for participation that will include the invited speakers and their topics.
+
+#### Invited speakers and topics
+
+| Speaker           | Modularity in...         | Slides                 |
+| ----------------- | ------------------------ | ---------------------- |
+| Catherine Dubois  | Proof Checking           | [slides](Dubois.pdf)   |
+| Georges Gonthier  | Large Proofs             | [slides](Gonthier.pptx)|
+| Till Mossakowski  | Ontologies               |                        |
+| Natarajan Shankar | Proof Assistants         | [slides](Shankar.pdf)  |
+| Doug Smith        | Software Synthesis       | [slides](Smith.ppt)    |
+| Nicolas M. Thiery | Mathematical Computation | [slides](Thiery.pdf)  |
+
+
+#### Organizers
+
+- Jacques Carette, McMaster University (carette@mcmaster.ca)
+- Dennis Müller, FAU Erlangen-Nürnberg (d.mueller@kwarc.info)
+- Florian Rabe, Jacobs University Bremen (florian.rabe@fau.de)
+
+### Abstracts
+
+#### Modularity in Proof Checking (Catherine Dubois)
+The essence of (automated) proof checking is to check proofs for
+correctness. A proof checker takes a proposition and a presumed proof
+and merely verifies  the proof, checking it for correctness. It is
+much simpler to verify a proof than finding it. 
+Proof checking can be done in a batch way or interactively, as part of
+an interactive theorem prover. For example it is triggered in Coq by
+the keyword that ends a proof script (e.g. Qed or Defined). Moving
+proof checking outside of theorem provers is explored and implemented
+for example within the Dedukti system. Proof checking may also include
+some proof reconstruction.
+
+We may wonder why we need proof checking. First publications in
+mathematics or computer science may contain errors. Second automated
+theorem provers as complex software are buggy and thus verifying their
+answers and proofs is very important. Proof assistants are also complex
+software and having some independent proof checkers - off the shelves -
+may also help to reduce the trusted base instead of proving the code of
+proof assistants (which is an impossible task). Proof checkers are simpler
+software than interactive or automated proof tools. Their code can be
+reasonably
+checked by crossed-reviews for example.
+
+Type theory reduces the problem of proof checking to the problem of
+type-checking in a programming language. Thus a proof is a
+lambda-term, it is  a correct proof of a formula if its type is
+exactly the formula to be proven, thanks to the proofs-as-programs
+analogy. In our
+presentation, we'll focus on that definition/dimension of proof
+checking.
+
+Modular systems in computer science are divided into components or
+modules with
+well-defined interfaces and dependencies as small as
+possible. Modularity requires also mechanisms to
+compose/compile/assemble the
+components together to obtain an executable software.
+There is no doubt that proof checkers are modular software according to
+the previous
+definition. Let us go further and apply the feature of components/modules to
+proofs. We can distinguish internal modularity and external
+modularity. Internal modularity provides mechanisms to structure large
+proofs (e.g. modules, inheritance) while external modularity provides
+mechanisms to interface proofs having different origins and build
+'composite proofs'. I will illustrate external modularity with
+Dedukti and a proof of Erathostenes sieves made of a Coq component and
+a HOL component verified by the Dedukti proof checker.
+
+#### Modularity for specification, ontologies, and model-driven engineering (Till Mossakowski) (CANCELED)
+Within the fields of software specification, ontologies,
+model-driven engineering, and others, different notions of modularity
+have been studied. It turns out that a semantics of these
+artefacts can be both given in terms of logical theories, as well
+as in terms of model classes.
+
+Our central hypothesis is that a good support for modularity
+should one the hand support both the model-theoretic and
+theory-based point of view. On the other hand, it should be
+applicable to a wide variety of (logical) languages.
+
+The Distributed Ontology, Modeling and Specification
+Language (DOL), standardised by the OMG, aims at providing a
+unified metalanguage for meeting these criteria.
+
+#### What is a Module? (Natarajan Shankar)
+A module is a functional subsystem with an interface through which it
+interacts with other subsystems.  A module could be a body of
+knowledge or a theory (e.g., vector spaces), a biological subsystem
+(e.g., the nervous system), an organizational unit (e.g., accounting),
+a physical component (e.g., steering wheel), or a software component
+(e.g., compiler).  In computing, modules appear in specification
+languages like Z and PVS; modeling languages like B, TLA+, and SAL;
+and programming languages like Ada and ML.  Module mechanisms serve
+several different purposes: packaging and reuse of related
+functionality, abstraction and encapsulation of state and internal
+representations, separate compilation, and composition.  We discuss
+some of the principles underpinning the design of module systems and
+accompanying composition and reasoning principles.
+
+#### Modular Knowledge in Software Synthesis (Doug Smith)
+Software synthesis tools support the translation of requirements into acceptable software de-
+signs. The requirements may be expressed logically, with a deductive design process, or the
+requirements may come in the form of datasets, with an inductive design process. This session
+focuses on modularity in software synthesis, and in particular on modular knowledge about re-
+quirements, software design, and the structure of the design process. We briefly outline some of
+the key forms of modularization that arise in these aspects of software synthesis.
+
+1 - Requirements
+
+For applications where mathematical correctness is important, requirements and high-level
+designs can be structured using formal logical specifications as finite presentations of theo-
+ries, which are composed using specification morphisms and colimits. For machine learning
+applications, the requirements come in form of structured data sets.
+
+2 - Software Design Knowledge
+
+Representations of software design knowledge allow developers to guide an automated synthe-
+sis system so that it can effectively translate requirement-level specifications into acceptable
+high-level designs. Transformations (replace specification or code patterns by other code
+patterns) and inference rules that relate logical goals with program structure (e.g. deduc-
+tive synthesis rules) provide some of the basic design knowledge modules for any synthesis
+system. Larger grain modules can capture reusable higher-level design knowledge: algorithm
+design theories, datatype specifications and refinements, formalized design patterns, and
+architectural patterns. These are used with deductive/refinement techniques to generate ini-
+tial designs from requirement-level specifications. Machine learning applications also exploit
+larger-grain patterns, such as linear regression models and neural networks. These provide a
+computation pattern (with parameters to-be-learned and chosen hyperparameters) that can
+be instantiated using methods for fitting models to the given data. More ad-hoc forms of de-
+sign knowledge include sketches, program templates, and schemata. These are used with (1)
+deductive/refinement techniques to generate instantiations from logical specifications, or (2)
+inductive generalization techniques that search a space of instances given concrete examples.
+
+3 - Derivations
+
+A software synthesis process that generates interesting software usually involves the compo-
+sition of many kinds of design knowledge and so it is relevant to consider the structuring of
+that composition, called a derivation. Derivations can be a sequence (or tree) of specifications
+where each is derived from its predecessor by applying a module of design knowledge. Typ-
+ically, the early knowledge applications in a derivation introduce the overall algorithmic or
+architectural structure and then many more knowledge applications are applied to improve
+performance and to fit the design to the target computational substrate.
+
+#### Modularity in Mathematical Computation (Nicolas Thiery)
+Over the last decades, a huge amount of computational software was
+developed for pure mathematics, in particular to support research and
+education. As for any complex ecosystem of software components, the
+ability to compose them has a multiplier effect on the expressive
+power, flexibility, and range of applications.
+
+The purpose of this session is to share experience on the many
+barriers to composability in computational mathematics, and how they
+are being tackled in various communities. Of particular interest will
+be the exploitation of knowledge to leverage some of the barriers.
+feedback from neighbor fields (proofs, data, knowledge) will be most
+welcome.

events/index.md

@@ -2,6 +2,7 @@
 layout: page
 title: KWARC - Events 
 ---
-The Academic Events we organize
+Some smaller academic events we have organized that do not have separate homepages:
 
-* [Tetrapod Workshop at FLOC-2018](/events/Tetrapod-2018)
+* [Tetrapod Workshop at FLOC-2018](Tetrapod2018/index.html)
+* [GI Jahrestreffen Fachgruppe Deduktionssystem und Logic in der Informatik](GILogicWorkshops/index.html)

index.md

@@ -5,11 +5,34 @@ title: Home
 
 The ability to *represent knowledge about the world* and to *draw logical inferences* is one of the central components of intelligent behavior, as a consequence, reasoning components of some form are at the heart of many artificial intelligence systems.
 
+#### Research
+
 The KWARC research group conducts research in knowledge representation and reasoning techniques with a view towards applications in knowledge management. 
 We extend techniques from [formal methods](http://kwarc.info/semantics.html#fm) so that they can be used in settings where formalization is either infeasible or too costly. 
 We concentrate on developing techniques for marking up the [structural semantics](http://kwarc.info/semantics.html#ssem) in technical documents. 
 This level of markup allows for offering interesting [knowledge management services](http://kwarc.info/projects/) without forcing the author to formalize the document contents.
 
+##### Approach: Corpus-based Meta-Mathematics
+In this title we have three components that warrant explanation: 
+1. **Mathematics**: we use the  mathematical knowledge and mathematical documents as a test
+  tube for our research as the knowledge and document structures are quite explicit and
+  overt and the content of mathematics is well-understood. Anything that has the same
+  properties we consider to be "mathematics" as well. 
+2. **Meta**: we develop Meta-Artefacts, i.e. we
+   * design **representation languages** (logics) that allow to talk *about* mathematical objects,
+   their properties, and relations,
+   * invent **algorithms** that analyze and transform these representations, and
+   * implement them in **end-user systems** that utilize both. 
+3. **Corpus-based**: we do this as a natural science by looking at data (i.e. corpora of
+documents and formalizations).
+
+##### KWARC Process
+We approach Corpus-Based Meta-Mathematics (iteratively) in three steps:
+1. **Analysis**: we analyze the corpora for patterns and structures.
+2. **Synthesis**: we design and build meta-artefacts (languages, algorithms, and systems)
+and derive data sets from the corpora.
+3. **Experimentation**: we evaluate the representation languages and algorithms on the
+   corpora and the systems on end users (mathematicians).
 
 #### Recent News ([see all](/news/))
  
@@ -18,3 +41,6 @@ This level of markup allows for offering interesting [knowledge management servi
         {% include post_link.html post=post %}
     {% endfor %}
 </ul>
+
+<!--  LocalWords:  endfor analyze
+ -->

people/achugh.md

+---
+layout: person
+
+title: Abhishek Chugh
+fullname: M.Sc. Abhishek Chugh
+pic: public/images/abchugh.png
+
+role: Research Engineer
+start_date: 2022-05
+
+publink: https://linkedin.com/in/abhishekchugh
+
+website: https://sophize.org
+affiliation: Sophize Foundation
+---
+
+### Description
+
+I am a software engineer and has worked on products such as Adobe Illustrator, Google Maps and Google Pay. I am passionate about organizing knowledge from different perspectives in a way that allows readers to effortlessly see all kinds of justifications for and against any claim. To further this goal, I started Sophize Foundation, a non-profit that is currently working towards building an open state-of-the-art [Mathematics library](https://sophize.org).
+
+### Research Focus
+
+As a KWARCie, I am very excited to help build systems and interfaces that will generate and present educational material tailored to each learner's specific needs.

people/ahambasan.md

@@ -7,6 +7,7 @@ fullname: Alexandru Hambasan
 role: bachelor-student
 pic: public/images/ahambasan.jpeg
 start_date: 2017-03
+end_date: 2018-01
 
 affiliation: Jacobs Unviersity Bremen
 ---

people/akohlhase.md

@@ -9,7 +9,13 @@ role: postdoc
 start_date: 2005-12
 end_date: 2014-08
 
+dblp: k/Kohlhase:Andrea
+researchgate: Andrea_Kohlhase2
+github: akohlhase
+mathhub: akohlhase
+zbmath: kohlhase.andrea
 publink: auto
+orcid: 0000-0001-5384-6702
 
 affiliation: Hochschule Neu-Ulm
 website: https://www.hs-neu-ulm.de/andrea-kohlhase/
@@ -46,4 +52,4 @@ human-spreadsheet interactions and decouple our semantic services from specific
 spreadsheet players like MS Excel.
 
 At the end of last year I started to make use of Kelly's Repertory Grid Technique. The
-example data set for the MathUI'13 paper you can find [here](http://www.kwarc.info/ako/ProcrustesAnalysis).
\ No newline at end of file
+example data set for the MathUI'13 paper you can find [here](http://www.kwarc.info/ako/ProcrustesAnalysis).

people/aschmidt.md

+---
+layout: person
+
+title: Annika Schmidt
+fullname: B.Sc. Annika Schmidt
+pic: public/images/aschmidt.png
+
+start_date: 2020-10
+end_date: 2021-11
+role: master-student
+affiliation: Computer Science, FAU Erlangen-Nürnberg
+
+NOpublink: auto
+
+NOwebsite:
+---
+### Description  
+
+I am a master student at [FAU Erlangen-Nürnberg](http://www.fau.de). Currently I am working on my master thesis at the [KWARC group](http://kwarc.info) and got employed there as a Hiwi to help with the AI-1 lecture.
+
+In 2015 I started studying Computer Science at [FAU Erlangen-Nürnberg](http://www.fau.de). While finishing my bachelor's degree I visited some master courses. My main interests are optimization and artificial intelligence. Also, I am very interested in knowledge management and gaining new knowledge.
+
+### Current Work
+
+My master thesis is about the formalization of set theory in [KWARC's MMT system](https://kwarc.info/systems/mmt/). To achieve this goal I use some old formalizations of set theory in Twelf. Since I just started the exact course of my master thesis is still unclarified.
+
+My work as a Hiwi mostly consists of cutting old lecture videos to make online lectures more attractive for students. Also, I give advice and help to come up with good questions for the students.
+
+### Contact
+
+Feel free to contact me at annika.as.schmidt@fau.de.