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
Select Git revision
  • master
  • zolekode-master-patch-26857
  • zolekode-master-patch-38209
  • zolekode-master-patch-54259
  • zolekode-master-patch-78201
5 results

Target

Select target project
  • kwarc/kwarc.info/www
  • richardmarcus/www
2 results
Select Git revision
  • master
  • patch-1
2 results
Show changes
Showing
with 437 additions and 78 deletions
---
layout: person
title: Ulrich Rabenstein
fullname: Ulrich Rabenstein
affiliation: Computer Science, FAU Erlangen-Nürnberg
fullname: M.Sc. Ulrich Rabenstein
pic: public/images/urabenstein.jpg
account: urabenstein
role: master-student
start_date: 2016-10
end_date: 2017-07
affiliation: Computer Science, FAU Erlangen-Nürnberg
---
### Description
I have written my master thesis as a member of the KWARC group. My task was to detect quantity expressions in STEM-documents and to build useful semantic services.
#### Thesis
[Meaning Extraction and Semantic Services in STEM-Documents -
A case study on Quantity Expressions and Units](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2017/urabenstein/Rabenstein.pdf)
---
layout: person
title: Vyacheslav Zholudev
fullname: Dr. Vyacheslav Zholudev
role: phd-student
pic: public/images/vzholudev.jpeg
role: phd-student
start_date: 2007-09
end_date: 2012-07
publink: auto
affiliation: ResearchGate
---
### Description
In July 2012 I have received my PhD in computer science at the Jacobs University.
### Thesis Title:
### Thesis Title
Enhancing XML Preservation and Workflows
\ No newline at end of file
### Current Affiliation?
ResearchGate
---
layout: project
menu_title: FormalCAD
title: "FormalCAD: Formal Methods and Semantic Technologies for Engineering Design
Processes"
shorttitle: FormalCAD
teaser: Towards a computer-supported, document-oriented process for systematic engineering design and a semantic help system for CAD systems.
start: 2012-04
end: 2015-02
people: mkohlhase,akohlhase,cjucovschi
active: false
start_date: 2012-04
end_date: 2015-02
publink: auto
people:
- mkohlhase
- akohlhase
- cjucovschi
collaborators:
- Lutz Schröder, FAU Erlangen
logo: public/dfg_logo.svg
funding: DFG
program: Normalverfahren
grantid: KO 2428/12-1
collaborators: Lutz Schröder, FAU Erlangen.
---
Systematic engineering design processes follow a series of standardized development stages that have many aspects in common with software engineering. In this analogy, CAD/CAM objects replace program code as the implementation stage of the development; however, other recognized development stages such as requirements or principle solutions are currently left largely informal and in fact are typically not laid down in machine-processable form at all. We propose to draw on the mentioned analogy and transfer methods from software engineering to engineering design in order to capture the full engineering design process formally and thus enhance in particular their reliability and reusability. We envision a document-oriented design process that integrates all stages of the development process from requirement specifications to CAD/CAM documents, and moreover incorporates background knowledge such as enterprise ontologies, industrial standards, and formalized geometric principles. In the FormalCAD project, we plan to develop the information architecture for such a process and support it with a tool that interfaces a CAD system with formal specification languages, ontology reasoners, and semantic document management systems, thus allowing for a comprehensive development methodology that supports completely formalized development strands, change and life-cycle management, as well as semantically interlinked semi-formal documents for documentation and certification. FormalCAD is a joint project with Prof.
---
layout: project
title: "ALMANAC: Argumentation Logics Manager & Argument Context Graph"
shorttitle: "ALMANAC"
teaser: Decision situations require individuals and organizations to choose between a multitude of options based on facts, opinions, and arguments about the situation at hand or similar ones. There is already a large set of prior work on the representation of knowledge, inference, and argumentations; the ALMANAC aims to a) bring order into the zoo of proposed formalisms, b) categorize their inter-relations, and c) benchmark them on real-world corpora.
active: false
start_date: 'January 2018'
end_date: 'February 2022'
publink: auto
people:
- mkohlhase
- dmueller
- cshi
- mrapp
funding: DFG
logo: public/dfg_logo.svg
program: Normalverfahren
grantid: KO 2428/18
proposal: http://kwarc.info/kohlhase/projects/almanac.pdf
---
Decision situations require individuals and organizations to choose between a multitude of options based on facts, opinions, and arguments about the situation at hand or similar ones. Current support systems are mostly fact-based and fail to take into account arguments found on the web or in the literature.
The SPP brings together a community of researchers who develop robust and scalable models for argumentations in human communication in all their complexity and imprecision. The ALMANAC project develops support for the logic-based pillar of this enterprise. There is already a large set of prior work on the representation of knowledge, inference, and argumentations and the SPP will no doubt develop more.
The first objective of the proposed ALMANAC project is to provide a unifying infrastructure so that the SPP projects and wider community can interoperate, compare results, and create joint logic resources. Concretely we propose to
1. bring order into the zoo of proposed formalisms,
2. categorize their inter-relations, and
3. benchmark them on real-world corpora
For this the ALMANAC project proposes to utilize the OMDoc/MMT framework developed by the proposer’s research group. The framework uses theory graphs for the modular representation of domain knowledge in logical languages and for logical formalisms themselves in meta-logics. Inter-logic relations can be modelled as theory-morphisms: truth-preserving mappings between theories. The ALMANAC project wants to provide the SPP with a “logic atlas” as a resource of explicitly represented formalisms and frameworks that can serve as a basis for integration of methods.
The second objective of the proposed ALMANAC project is to utilize the theory graph structure as a model for the contexts in multi-agent argumentations: theory graphs naturally provide “little ontologies” (the theories) that can be mutually exclusive and are interconnected by inclusions and views (in OMDoc/MMT). To augment them to full argumentation context graphs we want to add argumentation relations like attack, rebut, support, and undercut and study their ontological properties.
OMDoc/MMT is implemented by the MMT system, which serves as a (meta)-knowledge base and offers logical services like type/proof checking, inter-logic translation, and human-oriented browsing of corpora. MMT is integrated into the MathHub system which additionally offers user- and logic-corpus management facilities and can serve as the basis for logic-based challenges (Joint Tasks; the third objective of ALMANAC) that induce synergies between projects in the SPP and thus contribute to the coherence of the overall endeavor.
---
layout: project
title: arXMLiv
shorttitle: arXMLiv
active: true
teaser: Translating the arXiv to XML/HTML5
start_date: '2006'
publink: http://kwarc.github.io/bibs/arXMLiv
funding: internal
people:
- dginev
- mkohlhase
collaborators:
- Dr. Bruce Miller (NIST)
- various Jacobs University undergrads
logo: public/kwarc_logo.svg
website: http://corpora.mathweb.org
repository: https://github.com/dginev/CorTeX
---
The [Cornell e-print arXiv](http://arxiv.org) contains one of the largest corpora of
scientific literature in the world. Unfortunately, its contents are locked up in the
TeX/LaTeX format, which makes it nearly useless for knowledge management techniques. We
translate it to XML and "HTML5 with [MathML](http://www.w3.org/TR/MathML/)" via
[LaTeXML](https://dlmf.nist.gov/LaTeXML/) to have a basis for uncovering it's structural
semantics (see the [LLaMaPuN](/systems/llamapun/) project for details).
The actual corpus processing (and distribution to hundreds of worker machines) is
performed by the [CorTeX](https://github.com/dginev/cortex) system; see the [system
state/results on arXiv](https://corpora.mathweb.org/history/arxmliv/tex_to_html).
Applications of this include a mathematical search engine [MathWebSearch](/systems/mws/):
(live [demo on the arXMLiv data set](http://arxivsearch.mathweb.org)).
Unfortunately, we cannot re-distribute the results of the transformation freely due to
arXiv licensing policies. Therefore we have created the Special Interest Group for Math
Linguistics ([SIGMathLing](http://SIGMathLing.kwarc.info)) that can distribute the data
sets under an [NDA](https://sigmathling.kwarc.info/nda/) to
[SIGMathLing members](https://sigmathling.kwarc.info/member/).
But [arXiv](http://arxiv.org) is working together with us to make their offerings more
accessible see [arxiv labs](https://labs.arxiv.org/).
---
layout: project
title: "CoMMa: Corpus Meta-Mathematics"
shorttitle: CoMMa
active: true
teaser: Representing and Extracting the Meaning of Mathematical/Technical Documents
start_date: '2006'
funding: internal
people:
- mkohlhase
- dginev
- jfschaefer
- pzoleko
logo: public/kwarc_logo.svg
publink: auto
funding: internal
---
Many of the foundations of the wealth of western societies are laid down in mathematical/technical documents. Such are rich in structure and communicate complex meaning effectively and efficiently, but we do not understand the underlying knowledge structures and linguistic characteristics enough to extract the underlying meanings and represent them explicitly enough so that working with them can be supported by machines.
This leads to the [one brain barrier](/kohlhase/papers/ems13.pdf) in Science, Technology, Engineering, and Mathematics (STEM): instead of being machine-processable, mathematical/technical knowledge must always pass through a human brain for innovation, application, and education.
In the CoMMa project, we work towards remedying this problem for Mathematics (which can serve as a test tube for STEM documents) by applying methods from
##### Meta-Mathematics
i.e. employing languages that allow to talk about the concepts, objects, and models of mathematics. We employ the [OMDoc (Open Mathematical Documents)](/systems/OMDoc/) format for representing document and knowledge structures at all levels and with flexible formality, the [MMT system](/systems/mmt) for formalizing knowledge in a foundation-independent manner ([details and discussion](http://kwarc.info/kohlhase/papers/omdoc-semantics.pdf)).
##### Corpus-Linguistics
i.e. extracting meaning-carrying structures from documents at the scale of large, representative corpora. We prepare and manage large mathematical corpora in the [arXMLiv effort](/projects/arXMLiv/) and distribute math linguistic data sets via the [SIGMathLing initiative](http://sigmathling.kwarc.info). We contribute to the infrastructure for math linguistics with the [LLaMaPUn](/systems/llamapun/) library and the [KAT](/systems/kat/) annotation tool.
---
layout: default
title: Current Projects
menu_title: Current
menu_order: 101
---
## Current Projects ([past projects](/projects/past/))
to be generated here.
---
layout: project
title: "Digitaler Registerassistent"
shorttitle: "DiRegA"
teaser: Towards automating Register Courts via Symbolic and Subsymbolic AI
active: true
start_date: 'March 2024'
end_date: 'February 2027'
publink: auto
people:
- mkohlhase
- mrapp
- jfschaefer
funding: Bundesnotarkammer
logo: public/bnotk.jpg
website: https://www.direga.fau.de/
---
The DIREGA ( Digitaler Registerassistent) project conducts muti-disciplinary, foundational
research in Computer Science and the law. It studies the question if - and so how - legal
decisions can be supported - and even be automated - by symbolic AI and machine
learning. The legal application domain is register law.
The project is funded by the German Federal Chamber of Notaries (Bundesnotarkammer) in
coorpation with the Bavarian Chamber of Notaries (Bayrische Notarkammer) and the Bavarian
State Ministry of Justice (Bayerischen Staatsministerium der Justiz).
For details (in German) see https://www.direga.fau.de/
---
layout: default
title: Past Projects
menu_title: Past
menu_order: 102
---
## Completed Projects ([current projects](/projects/current/))
{% assign projects = site.pages | where: "layout", "project" | where_exp: "project", "project.end != null" | sort: "start" %}
{% include projects_list.html %}
---
layout: default
title: KWARC Projects
---
<h2>Current Projects of the KWARC Group</h2>
{% assign projects = site.pages | where: "layout", "project" | where_exp: "project", "project.end == null" | sort: "start" %}
{% include projects_list.html %}
---
layout: project
menu_title: JEM
title: "JEM: Joining Educational Mathematics"
start: 2006
end: 2009
shorttitle: JEM
teaser: Coordination of European content enrichment activities in the area of mathematics
active: false
start_date: '2006'
end_date: '2009'
publink: auto
people:
- mkohlhase
- nmueller
- cmueller
logo: public/eu_logo.png
funding: EU
program: eContentPlus Thematic Network
homepage: http://calc.mathstat.helsinki.fi/jem/en/about/
people: mkohlhase
website: http://calc.mathstat.helsinki.fi/jem/en/about/
---
The network assembles leading developers of semantic web technologies for the
representation of mathematics, mathematics content stakeholders and experienced
distributors of software and eLearning solutions.
---
layout: project
menu_title: LATIN
title: "LATIN: Logic Atlas & Integrator"
start: 2009
end: 2012
shorttitle: LATIN
teaser: Building a theory graph of logic represesentations.
active: false
start_date: '2009'
end_date: '2012'
publink: auto
people:
- mkohlhase
- frabe
- fhorozal
- miancu
collaborators:
- Till Mossakowski, DFKI Bremen
logo: public/dfg_logo.svg
funding: DFG
program: Normalverfahren
grantid: KO 2428/9-1
people: mkohlhase,frabe,fhorozal,miancu
collaborators: Till Mossakowski, DFKI Bremen
---
LATIN aims at developing methods, techniques, and tools for interfacing logics and proof
......
---
layout: project
menu_title: Logosphere
title: "Logosphere: Formal Digital Libraries"
start: 2003
end: 2006
shorttitle: Logosphere
teaser: Integrating Theorem Prover Libraries through Meta-logical Frameworks
active: false
start_date: '2003'
end_date: '2006'
publink: auto
people:
- mkohlhase
- inormann
collaborators:
- Carsten Schürmann, Yale University
- Frank Pfenning, CMU
- Natarajan Shankar, SRI International
- Sam Owre, SRI International
funding: NSF
program: ITR
grantid: CCR-ITR-0325808
people: mkohlhase
collaborators: Carsten Schürmann (Yale University), Frank Pfenning (CMU) Natarajan Shankar, Sam Owre (SRI International)
---
Mathematical knowledge is at the core of science and engineering. The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing a Formal Digital Library called Logosphere, a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. Logosphere emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems. The Logosphere infrastructure is designed to be scalable with respect to the size of the knowledge base as well as the diversity of formalisms.
......
---
layout: project
title: MaMoReD
shorttitle: MaMoReD
teaser: Flexiformalizing Mathematical Models as Research Data
active: true
start_date: '2016-11'
publink: http://kwarc.github.io/bibs/MaMoReD
people:
- mkohlhase
- dmueller
- frabe
- tpollinger
collaborators:
- Dr. Thomas Koprucki (WIAS Berlin)
- Dr. Wolfram Sperber (FIZ Karlsruhe)
- Dr. Karsten Tabelow (WIAS Berlin)
- Dr. Olaf Teschke (FIZ Karlsruhe)
logo: public/kwarc_logo.svg
funding: internal
---
The MaMoReD projects studies whether and how the flexiformalization of mathematical
mathematical models can allow them to be treated as research data, i.e. to be amenable to
mathematical knowledge management methods.
### Workshops
<!-- don't introduce new lines here, it confuses the markdown processor; add two spaces at the end of a line for a line break -->
1. 2018, January, 15-17 in Erlangen
**Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow
**Topics**
* stochastic models (continued)
* preparation of grant proposal
1. 2017, November, 4-8 at WIAS Berlin
**Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow
**Topics**
* generation of Python and C code from MMT formalizations of models
* formal language for solution strategies of mathematical models
* stochastic models
1. 2017, March, 21-24 at WIAS Berlin
**Participants**: Kohlhase, Koprucki, Müller, Rabe, Sperber, Tabelow, Teschke
**Topics**
* preparation of journal paper on abstract definition of models
* formalization of units and quantities in MMT
1. 2017, January, 16-19 in Erlangen
**Participants**: Kohlhase, Koprucki, Müller, Rabe, Tabelow
**Topics**
* MMT tutorial
* formalization of van Roesbroock Modell for charge transport in semi-conductors in MMT
* formalizing complex device geometries
* survey of state of the art in mathematical modeling
* generation of LaTeX documents from MMT formalizations of models
1. 2016, November 9. at WIAS Berlin
**Participants**: Kohlhase, Koprucki, Tabelow
**Topics**
* Models as Research Data
* Theory Graphs and Models
* Mathematical Knowledge Management for Models
---
layout: project
menu_title: MathSearch
title: "MathSearch: Analyse und Suche in mathematischen Formeln"
shorttitle: MathSearch
teaser: Methods for information extraction and information retrieval for mathematical documents with the aim of providing semantically enhanced interaction for Zentralblatt Math and the arXiv.
start: 2012-03
end: 2015-02
active: false
start_date: 2012-03
end_date: 2015-02
publink: auto
people:
- mkohlhase
- dginev
logo: public/leibniz_logo.svg
funding: Leibniz Foundation
program: SAW
grantid: SAW-2012-FIZ_KA-2
people: mkohlhase,dginev
---
The MathSearch Project develops a semantic search engine for mathematics in collaboration
......@@ -17,6 +27,6 @@ with the [ZBMath Group](https://zbmath.org/about/) at
[Leibniz Foundation](https://www.leibniz-gemeinschaft.de/) as SAW project
AW-2012-FIZ_KA-2.
We have deployed an instance of [MathWebSearch](/projects/mws/) engine as part of the
We have deployed an instance of [MathWebSearch](/systems/mws/) engine as part of the
[ZBMath Information System](http://zbmath.org) (see the "Formulae" tab there), and we have
started the [SMGloM](/projects/smglom/).
started the [SMGloM](/systems/smglom/).
---
layout: project
title: MathDataHub
shorttitle: MDH
teaser: A Collaboration Project with Ljubljana University
active: false
start_date: 2020-01
end_date: 2021-12
people:
- mkohlhase
- frabe
- kbercic
- twiesing
funding: DAAD
program: Collaboration Grant
logo: public/daad_logo.svg
---
Modern mathematical research increasingly depends on collaborative tools, computational environments, and online databases, and these are changing the way mathematical research is conducted and how it is turned into applications. For example, engineers now use mathematical tools to build and simulate physical models based on systems of differential equations with millions of variables, combining building blocks and algorithms taken from libraries shared all over the internet.
The KWARC group at FAU Erlangen-Nürnberg and the group at Ljubljana University collaborate on the establishment of MathDataHub, a semantic portal for mathematical data sets.
Technical directions on adding a project
------------------------------------------
To add a new project, create a file in this directory, taking the existing files as
To add a new system, create a file in this directory, taking the existing files as
examples.
Each post needs some specific parameters:
* **layout** use `project` or `software`
* **layout** use `project`
* **title** the title of the project
* **subtitle** (optional) a subtitle. It will be adjuncted to your title in the post
link and just under the title in the post page
* **shorttitle** the short title of the project, used for project chips
* **teaser** (optional) a one-line description for the overview
* **people** (optional) the KWARC people involved in this
* **collaborators** (optional) the outside collaborators
* **start** (optional) the project start date
* **end** (optional) the project end date
* **logo** (optional) a (local) path to the logo of a project
* **active** boolean indicating if the project is active
* **start_date** the system start date (YYYY[-MM])
* **end_date** (optional) the system end date (YYYY[-MM])
* **people** (optional) a list of KWARC people involved in this
* **collaborators** (optional) a list of non-KWARC people involved in this
* **funding** (optional): the funding body, *DFG*, *Leibniz Foundation*, *EU*, *Industry*
use *internal* for projects that do not have funding (yet), but are project-organized.
* **program** (optional): the funding program
* **grantid** (optional): the project identifier of the funder, e.g. `KO 2428/13-1`
* **homepage** (optional): the project home page
* **website** (optional): the project home page
---
layout: default
title: Completed Projects
permalink: /projects/completed/
---
{% assign projects = site.pages | where: "layout", "project" | where: "active", false | sort: "end_date" | reverse %}
#### Completed, externally funded Projects
<ul class="collection">
{% for item in projects %}
{% if item.funding %} {% include psitem.html item=item %} {% endif %}
{% endfor %}
</ul>
#### Former Internal Projects
We also organize some of our research and development into Projects,
<ul class="collection">
{% for item in projects %}
{% unless item.funding %} {% include psitem.html item=item %} {% endunless %}
{% endfor %}
</ul>
#### System Projects
Completed projects that focused on building particular systems can be found under [KWARC Systems](/systems/historic/).
---
layout: default
title: Projects
permalink: /projects/
---
{% assign projects = site.pages | where: "layout", "project" | where: "active", "true" | sort: "start_date" %}
#### Projects with external funding
<ul class="collection">
{% for item in projects %}
{% unless item.funding == 'internal' %}
{% include psitem.html item=item %}
{% endunless %}
{% endfor %}
</ul>
#### Internal Projects
We also organize some of our research and development as projects as well, sometimes to
prepare for funding applications, other times to have a framework for collaborating with
external researchers:
<ul class="collection">
{% for item in projects %}
{% if item.funding == 'internal' %}
{% include psitem.html item=item %}
{% endif %}
{% endfor %}
</ul>
#### System Projects
Internal projects that are focused on building particular systems can be found under [KWARC Systems](/systems/).
File added