events/GILogicWorkshops/2021/index.md

+---
+layout: page
+title: GI Meeting Deduction and Logic
+---
+
+### Online Meeting in Spring 2021
+
+The meeting took place online on March 26.
+The call for contributions is [here](cfp.txt).
+The call for participation is [here](cfpart.txt).
+
+The program consisted of 3 sessions of zoom talks each followed with a break in [gather.town](https://gather.town).
+
+#### Session 1: 10:00 - 12:15 (chair: Sergey Goncharov)
+
+* 10:00: Ana Sokolova, **Invited talk**: Algebraic Traces for Probability and Nondeterminism [slides (if any)](sokolova.pdf)
+* 10:45: David Fuenmayor,	Paraconsistent and paracomplete logics in Isabelle/HOL [slides (if any)](fuenmayor.pdf)
+* 11:05: Florian Bruse and Martin Lange and Marco Sälzer, On Finite Convergence of Fixpoints in the Modal Mu-Calculus [slides (if any)](2021/saelzer.pdf)
+* 11:25: Ali Farjami, Normative Reasoning: A Computational Challenge [slides (if any)](farjami.pdf)
+* 11:45: *break with free discussion in gather.town*
+
+#### Session 2: 13:00 - 15:15 (chair: Claudia Schon)
+
+* 13:00: Dov Gabbay and Ross Horne, **Invited talk**: Analytic Proof Calculi for the Notion of Failure [slides (if any)](gabbay.pdf)
+* 13:45: Christoph Benzmüller and David Fuenmayor, Value-oriented Legal Argumentation in Isabelle/HOL [slides (if any)](benzmueller.pdf)
+* 14:05: Claudia Schon and Sophie Siebert and Frieder Stolzenburg, Negation in Cognitive Reasoning [slides (if any)](siebert.pdf)
+* 14:25: Felix Weitkämper, A new role for finite model theory in statistical relational AI [slides (if any)](weitkaempfer.pdf)
+* 14:45: *break with free discussion in gather.town*
+
+#### Session 3: 15:15 - 17:30 (chair: Olaf Beyersdorff)
+
+* 15:15: Marl Joos and Tobias Philipp,	Mitigation of Cache Side Channel Attacks with Answer Set Programming [slides (if any)](joos.pdf)
+* 15:35: Mario Wenzel, Microlog - Microcontroller programming using Datalog [slides (if any)](wenzel.pdf)
+* 15:55: Muhammad Usama Sardar and Christof Fetzer, Understanding Remote Attestation in Intel SGX and TDX via Formal Verification [slides (if any)](sardar.pdf)
+* 16:15: Thomas Zeume, Teaching Logic with Iltis [slides (if any)](zeume.pdf)
+* 16:35: Lena Katharina Schiffer, Expressive Power of Combinatory Categorial Grammars [slides (if any)](schiffer.pdf)
+* 16:55: *break with free discussion in gather.town*
+
+#### Business meetings: 17:30 - 18:30
+
+* 17:30: Business meetings (Mitgliederversammlungen) of the GI groups
+
+----------------------------------------
+
+### Canceled meeting in Fall 2020
+
+The meeting was originally planned to take place in-person in Erlangen from 30.09.2020 to 02.10.2020.
+But after discussions among the speakers of the GI groups and the local organizers, it was postponed to Spring 2021 and eventually replaced with an online meeting.

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
-
-### Organization
-
-#### 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)
-
-#### Location
-[Federated Logic Conference 2018, Oxford](http://www.floc2018.org/), July 13.
-
-#### Format
-
-- There will be 8 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
-
-Invitations in progress
-
-#### Procedures for selecting papers
-  The organizers will select invited speakers and topics.
-  No selection of submissions is needed.
-
-#### Dissemination
-  A report will be written after the workshop that includes abstracts of the invited talks 
-  and the highlights of the discussions during the workshop.

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)