Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • kwarc/kwarc.info/www
  • richardmarcus/www
2 results
Show changes
Showing
with 269 additions and 19 deletions
File added
File added
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
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.
File added
File added
---
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
File added
File added
File added
File added
File added
......@@ -35,23 +35,21 @@ Of particular interest are
#### 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
| 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 (f.rabe@jacobs-university.de)
- Florian Rabe, Jacobs University Bremen (florian.rabe@fau.de)
### Abstracts
......@@ -177,7 +175,7 @@ ically, the early knowledge applications in a derivation introduce the overall a
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
#### 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
......
......@@ -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)
......@@ -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
-->
---
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.
......@@ -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
---
......
......@@ -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).
---
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.
---
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
......@@ -14,8 +14,8 @@ 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:
......