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

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

hiring/almanac-phd.md

+---
+layout: jobad
+title: ALMANAC Ph.D. Student or PostDoc (meta-logics for argumentation)
+posted: 2017-06-21
+status: open
+requirements: M.Sc (or equivalent) and a love for logic, language, and argumentation.
+---
+We are looking for a Ph.D. student or a PostDoc in the
+[ALMANAC Project](/projects/almanac/) positions can be half- or full-time. 

hiring/drupal-dev.md

@@ -2,7 +2,6 @@
 layout: jobad
 title: Drupal Developer (student)
 posted: 2017-08-21
-status: open
 requirements: experience or interest in Drupal
 ---
 We are looking for a Drupal developer (PHP, CSS) to help with front-end development of the [MathHub.info](http://mathhub.info) system. 

hiring/index.md

@@ -10,8 +10,10 @@ The KWARC group is constantly looking for good developers and Ph.D. students.
     {% for item in jobads %}
         {% if item.status contains 'open' %}
 	       <li class="collection-item">
-               <a href="{{jobad.url}}" class="title">{{jobad.title}}</a>
+               <a href="{{item.url}}" class="title">{{item.title}}</a>
            </li>
         {% endif %}
     {% endfor %}
 </ul>
+
+Candidates interested in the positions above should introduce themselves and inquire for further information by sending email with the usual documents to michael.kohlhase@fau.de

hiring/oaf-phd.md

 ---
 layout: jobad
-title: OAF Ph.D. Student (formalization)
+title: OAF Ph.D. Student (formalization of theorem prover logics/libraries)
 posted: 2017-06-21
 status: open
-requirements: M.Sc (or equivalent)
+requirements: M.Sc (or equivalent), interest in logics/theorem proving
 ---
-We are looking for a Ph.D. student in the [OAF Project](/projects/oaf/). 
+We are looking for a Ph.D. student in the [OAF Project](/projects/oaf/). Similar projects
+are in the pipeline; funding for the whole Ph.D. project is ensured.
+
+Candidates interested in the positions should introduce themselves and inquire for further information by sending email with the usual documents to michael.kohlhase@fau.de
+ 

hiring/odk-phd.md

+---
+layout: jobad
+title: OpenDreamKit Ph.D. Student/PostDoc (Math Modeling for Math System Integration)
+posted: 2017-06-21
+status: open
+requirements: M.Sc (or equivalent) and an interest in mathematics, computation, and system integration.
+---
+We are looking for a Ph.D. student or a PostDoc in the
+[OpenDreamKit Project](/projects/odk/) positions can be half- or full-time. 
+
+Similar projectsare in the pipeline; funding for the whole Ph.D. project is ensured.
+
+Candidates interested in the positions should introduce themselves and inquire for further information by sending email with the usual documents to michael.kohlhase@fau.de
+ 

hiring/web-frontend-dev.md

+---
+layout: jobad
+title: Web Frontend Developer (student)
+posted: 2018-03-22
+status: open
+requirements: experience or interest in HTML, CSS, JavaScript frameworks like jQuery and angular.js 
+---
+We are looking for a Web front-end developer (HTML, CSS, JS) for  the [MathHub.info](http://mathhub.info) system. 

index.md

@@ -5,16 +5,42 @@ 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/))
  
 <ul class="collection">
     {% for post in site.posts limit:5 %}
-        {% include post_link.html %}
+        {% include post_link.html post=post %}
     {% endfor %}
 </ul>
+
+<!--  LocalWords:  endfor analyze
+ -->

news/index.html

@@ -7,9 +7,9 @@ source: _posts/
 <div class="posts">
     <ul class="collection">
         {% for post in paginator.posts %}
-            {% include post_link.html %}
+            {% include post_link.html post=post %}
         {% endfor %}
     </ul>
 </div>
 
-{% include pagination.html %}
\ No newline at end of file
+{% include pagination.html paginator=paginator %}
\ No newline at end of file

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,6 +9,14 @@ 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/
 ---
@@ -44,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.

people/cdavid.md

@@ -8,6 +8,8 @@ pic: public/images/cdavid.jpeg
 role: master-student
 start_date: 2008-09
 end_date: 2012-02
+
+publink: auto
 ---
 
 ### Description

people/cjucovschi.md

 ---
 layout: person
 
-title: Constantin Jucovschi
-fullname: M.Sc. Constantin Jucovschi
+title: Constantin Jucowski
+fullname: M.Sc. Constantin Jucowski
 pic: public/images/cjucovschi.jpeg
 
 role: phd-student
 start_date: 2007-10
 
+publink: auto
+
 affiliation: Computer Science, FAU Erlangen-Nürnberg
 ---
 
 ### Description
-Constantin Jucovschi Ph.D. Student of Computer Science at FAU Erlangen supervised by
-Prof. Michael Kohlhase. 
+Constantin Jucowski, Ph.D. Student of Computer Science at FAU Erlangen supervised
+externally by Prof. Michael Kohlhase. 
 
 As of 2007 I am participating in various projects within the KWARC group, namely: SIDER:
 main developer of the xText based framework for developing semantic IDEs. NWERC 2010:

people/clange.md

@@ -9,6 +9,8 @@ role: phd-student
 start_date: 2008-07
 end_date: 2012-08
 
+publink: auto
+
 website: https://langec.wordpress.com/about/
 affiliation: Enterprise Information Systems, Fraunhofer IAIS Bonn
 ---

people/cmueller.md

@@ -10,6 +10,8 @@ start_date: 2006-09
 end_date: 2010-05
 
 affiliation: ti&m Frankfurt
+
+publink: auto
 ---
 
 ### Description