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 428 additions and 112 deletions
---
layout: system
menu_title: KAT
title: "KAT: An Annotation Tool for STEM Documents"
start: 2013-06
people: twiesing
title: "KAT: KWARC Annotation Tool"
shorttitle: KAT
teaser: An Annotation Tool for STEM Documents
start_date: 2013-06
end_date: 2017-06
orphan: true
people:
- mkohlhase
- twiesing
supported-by:
- mathsearch
logo: public/kwarc_logo.svg
repository: https://github.com/KWARC/KAT
publink: http://kwarc.github.io/bibs/kat
---
KAT is an annotation-ontology independent annotation tool for HTML5 documents. It can even annotate MathML.
KAT is an annotation-ontology independent annotation tool for HTML5 documents. It can
even annotate MathML. We use it for maths corpus linguistics.
---
layout: system
menu_title: Krextor
title: Krextor
start: 2008-02
end: 2010-09
people: clange
shorttitle: Krextor
teaser: An extensible XSLT-based framework for extracting RDF from XML.
start_date: 2008-02
end_date: 2010-09
people:
- clange
webpage: https://github.com/EIS-Bonn/krextor/wiki
repository: https://github.com/EIS-Bonn/krextor
publink: http://kwarc.github.io/bibs/krextor
---
Krextor, the ​KWARC RDF Extractor, is an extensible XSLT-based framework for extracting RDF from XML, supporting multiple input languages as well as multiple output RDF notations. See
Krextor, the ​KWARC RDF Extractor, is an extensible XSLT-based framework for extracting RDF from XML, supporting multiple input languages as well as multiple output RDF notations.
---
layout: system
menu_title: LLaMaPuN
title: "LLaMaPuN: Language and Mathematics Processing and Understanding"
start: 2008-11
people: mkohlhase,dginev,jfschaefer,itoloaca
title: "LLaMaPuN: Language and Mathematics Processing and Understanding"
shorttitle: LLaMaPuN
teaser: A RUST library for math corpus linguistics.
start_date: 2008-11
people:
- mkohlhase
- dginev
- jfschaefer
- itoloaca
supported-by:
- mathsearch
logo: public/kwarc_logo.svg
repository: https://github.com/KWARC/LLaMaPUn/
publink: http://kwarc.github.io/bibs/llamapun
---
The LaMaPUn project investigates the structure and meaning of scientific/technical
documents and builds tools for extracting semantic representations from them that can be
The [LLaMaPUn library](https://github.com/KWARC/LLaMaPUn/) is a
[RUST](https://www.rust-lang.org) library that provides a wide range of processing
tools for natural language and mathematics.
It can be used to investigate the structure and meaning of scientific/technical
documents and to build tools for extracting semantic representations from them that can be
used to enhance access to and interaction with document corpora.
The LLaMaPUn library consists of a wide range of processing tools for natural language and
mathematics. Its repository is at https://github.com/KWARC/LLaMaPUn/
In particular, the LLaMaPUn library is used on the
[arXMLiv](https://www.kwarc.info/projects/arXMLiv/) data set, which is a translation
of the [arxiv](https://arxiv.org/) corpus to "HTML5 with [MathML](https://www.w3.org/TR/MathML/)".
Some of the library's features are:
* Plaintext generation with many options (unicode normalization, word stemming, custom handling of e.g. `math` nodes, ...)
* Word/Sentence tokenization
* Support for standard NLP tools (token models for GloVe, POS tagging with SENNA, ...)
* Mapping between plaintext offsets and HTML nodes (using the DNM data structure)
For a more complete overview, take a look at the [README file](https://github.com/KWARC/llamapun/blob/master/README.md).
---
layout: system
menu_title: MathHub
title: MathHub
title: MathHub.info
shorttitle: MathHub
teaser: A portal for active mathematical documents and an archive for flexiformal mathematics.
start: 2008-08
start_date: 2008-08
people:
- mkohlhase
- akohlhase
- cjucovschi
- twiesing
- kbercic
supported-by:
- mathsearch
- oaf
- odk
- latin
- mdh
logo: public/mathHubLogo.png
website: http://mathhub.info
repository: https://github.com/KWARC/mathhub
homepage: http://mathhub.info
people: mkohlhase,akohlhase,cjucovschi
publink: http://kwarc.github.io/bibs/mathhub
---
MathHub.info is a portal for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with mathematical documents and knowledge
[MathHub.info](http://mathhub.info) is a portal for active mathematical documents and an
archive for flexiformal mathematics. It offers a rich interface for reading, writing, and
interacting with mathematical documents and knowledge.
The [MathHub.info](http://mathhub.info) system consists of a
* [repository manager](http://gl.mathhub.info) for mathematical archives based on [GitLab](http://gitlab.com) that handles user management, access control, and versioning.
* [knowledge management process](https://mmt.mathhub.info) based on the [MMT System](http://uniformal.github.io) that provides scalable knowledge management services and math presentation.
* various indices and data stores including [MathWebSearch](/systems/mws/).
* a web front end compositor that combines these into a uniform web experience.
* some special applications like a [multilingual glossary](https://mathhub.info/mh/glossary) and a [math dictionary](https://mathhub.info/mh/dictionary) based on the [SMGloM](/systems/smglom/) data set.
[MathHub.info](http://mathhub.info) serves as the main data repository for the [OAF](/projects/oaf) and [SMGloM](/systems/smglom/) projects and (the KWARC part of the [OpenDreamKit](/projets/odk/) project.
......@@ -7,18 +7,21 @@ examples.
Each post needs some specific parameters:
* **layout** use `system`
* **title** the title of the system
* **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 system, used for System 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 system start date
* **end** (optional) the system end date
* **pillar** (optional) the pillar (in the sense of http://kwarc.info/research) of the
system); use one of `semantization`, `KMR`, or `foundations`.
* **redirect_from** (optional) not needed for new systems, this is just the redirect
link from old activities pages on the former site.
* **funding** (optional): the funding body, *DFG*, *Leibniz Foundation*, *EU*, *Industry*
* **homepage** (optional): the system home page
* **repos** (optional): the system repository
* **logo** (optional) a (local) path to the logo of a system
* **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
* **supported-by** (optional) a list projects that have provided funding that supports
this project. Use the file names of the project to reference them.
* **website** (optional): the system home page
* **repository** (optional): the system repository
A system is considered active, iff it has no end date.
---
layout: default
title: Historic Systems
menu_title: Historic
menu_order: 2
permalink: /systems/historic/
---
## Historic Systems ([active systems](/systems/active/))
The KWARC group has developed various added value services based on OMDoc-encoded content,
including a mathematical knowledge base, a semantic search engine, management of change, a
......@@ -12,11 +10,12 @@ semantic wiki, mathematical web services, and invasive OMDoc editing
technologies. Furthermore, the group works on the utilization of OMDoc to provide Logic
Interoperability and to establish scientific Communities of Practice.
listing to be generated here.
{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
<ul class="collection">
{% for item in systems %}
{% if item.end_date %}
{% include psitem.html item=item %}
{% endif %}
{% endfor %}
</ul>
\ No newline at end of file
---
layout: default
title: Systems and Libraries
permalink: /systems/
---
{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
<ul class="collection">
{% for item in systems %}
{% unless item.end_date %}
{% include psitem.html item=item %}
{% endunless %}
{% endfor %}
</ul>
---
layout: page
title: Orphaned Systems up for Adoption
permalink: /systems/orphans/
---
Many of the KWARC projects are the work of students and become orphaned when these move on
to greener pastures (e.g. when they graduate). We put these systems up for adoption bt new
students. If you are interested, please contact someone from the KWARC group, we would be
happy to help you understand the development opportunities and get involved.
{% assign systems = site.pages | where: "layout", "system" | sort: "start_date" %}
<ul class="collection">
{% for item in systems %}
{% if item.orphan %}
{% include psitem.html item=item %}
{% endif %}
{% endfor %}
</ul>
\ No newline at end of file
---
layout: system
menu_title: MMT
title: "MMT: Meta Meta Theories/Meta Meta Tool"
title: "MMT"
shorttitle: MMT
teaser: A framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.
people: frabe,dmueller,twiesing,miancu,fhorozal
start_date: 2011-03
people:
- frabe
- dmueller
- twiesing
- miancu
- fhorozal
- mkohlhase
- nroux
supported-by:
- oaf
- odk
- latin
- mathsearch
logo: public/mmt_logo.svg
publink: http://kwarc.github.io/bibs/mmt
website: https://uniformal.github.io/
repository: https://github.com/Uniformal/MMT
---
MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. It achieves a high level of generality by systematically avoiding a commitment to a particular syntax or semantics. Instead, individual language features (e.g., λ-abstraction, conjunction, etc.) and syntax features (keywords, notations, etc.) are defined as separate, reusable modules, from which individual languages are assembled. These modules can be declarative by specifying features as Mmt theories or programmatic by providing individual rules as plugins.Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level. These include knowledge management algorithms (e.g, IDE, search, change management) as well as logical algorithms (e.g., parsing, type reconstruction, module system). Thus, we can use MMT to obtain strong implementations of declarative languages at extremely low cost.Moreover, the focus on modularity and language-independence enables system integration, where MMT can mediate the exchange of knowledge across different foundational systems and concrete syntaxes.See here for the MMT homepage.
---
layout: system
menu_title: MathWebSearch
title: "MathWebSearch a Mathematical Search Engine"
pillar: KMR
start: 2005
people: mkohlhase,isucan,cprodescu,rhambasan,ahambasan
shorttitle: MWS
title: MathWebSearch
teaser: A Mathematical Search Engine
start_date: '2005'
orphan: true
people:
- mkohlhase
- isucan
- cprodescu
- rhambasan
- ahambasan
- twiesing
supported-by:
- mathsearch
- odk
- oaf
<!-- logo: public/kwarc_logo.svg -->
website: http://search.mathweb.org
repository: https://github.com/MathWebSearch
publink: http://kwarc.github.io/bibs/mws
---
The MathWebSearch system (MWS) is a content-based search engine for mathematical
formulae. It indexes MathML formulae, using a technique derived from automated theorem
proving: Substitution Tree Indexing. Find more information at the
[Project Overview Page](http://search.mathweb.org) or the
[GitHub Repository](http://githhub.com/KWARC/mws).
proving: Substitution Tree Indexing. With this indexing technique MWS can answer
unification queries extremely efficiently (30-100 ms) on large sets of formulae (in the
Gigaformula range); but the index (up to 50GiB) needs to be kept in main memory.
MWS is the [formula search engine](https://zbmath.org/formulae/) employed in
[Zentralblatt Math](http://zbmath.org); see a
[demo on a mathematical subset](http://arxivsearch.mathweb.org) of the
[arXMLiv data set](/projects/arXMLiv/) [further demos](http://search.mathweb.org).
The MathWebSearch system is Open Source,
[developed on GitHub](https://github.com/MathWebSearch), and is (by now) easily deployable via
a set of docker containers. We can give your project a search interface like the
[nLab search](https://nlabsearch.mathweb.org/) for [nLab](https://ncatlab.org/) at the
cost of theming the [user interface](https://github.com/MathWebSearch/frontend) and
[building a harvester](https://github.com/MathWebSearch/nlab_harvester).
---
layout: system
menu_title: OMDoc
title: "OMDoc: Open Mathematical Documents"
teaser: A markup format and data model for Open Mathematical Documents. It serves as semantics-oriented representation format and ontology language for mathematical knowledge.
homepage: http://omdoc.org
repository: http://github.com/OMDoc
people: mkohlhase
shorttitle: OMDoc
teaser: A markup format and data model for Open Mathematical Documents and Knowledge
start_date: '1998'
people:
- mkohlhase
- miancu
- nmueller
- frabe
supported-by:
- Jem
- mathsearch
- omoc
- openmath-tn
- logosphere
- once-cs
logo: public/omdoc_logo.png
website: http://omdoc.org
repository: https://github.com/OMDoc
publink: http://kwarc.github.io/bibs/omdoc
---
OMDoc is a markup format and data model for Open Mathematical Documents. It serves as semantics-oriented representation format and ontology language for mathematical knowledge.
OMDoc is a markup format and data model for Open Mathematical Documents. It serves as
semantics-oriented representation format and ontology language for mathematical
knowledge. The formal part of OMDoc has been refined into the
[MMT format](https://uniformal.github.com), and we use the
[MMT System](https://uniformal.github.com) as the reference implementation.
We are currently working on extending MMT to cover the full flexiformal coverage of
OMDoc.
---
layout: system
menu_title: OpenMathMap
title: OpenMathMap
shorttitle: OpenMathMap
teaser: A Map of Mathematics
start: 2013-06
start_date: 2013-06
end_date: 2015-06
orphan: true
people:
- mkohlhase
supported-by:
- mathsearch
logo: public/kwarc_logo.svg
website: http://map.mathweb.org
repository: https://github.com/KWARC/openmathmap/
homepage: http://map.mathweb.org
people: mkohlhase
---
OpenMathMap project, a recognizable, interactive map of mathematical areas from the MSC an Zentralblatt Publication Data.
OpenMathMap project, a recognizable, interactive map of mathematical areas from the MSC an
Zentralblatt Publication Data. A demo is (sometimes) running on http://map.mathweb.org
---
layout: system
menu_title: sTeX
title: "sTeX: Semantic Markup for LaTeX"
pillar: semantization
start: 2004-09
people: mkohlhase,dginev
shorttitle: sTeX
start_date: 2004-09
people:
- mkohlhase
- dginev
- twiesing
collaborators:
- Dr. Bruce Miller (NIST)
supported-by:
- sissi
- mathsearch
- odk
logo: public/kwarc_logo.svg
repository: https://github.com/KWARC/sTeX
publink: http://kwarc.github.io/bibs/sTeX
---
The TeX/LaTeX workflow is deeply embedded into mathematical practice. Therefore the sTeX
system allows to embed [/structural semantics](/research/structural-semantics) into documents. For details see the [sTeX project on GitHub](https://github.com/KWARC/sTeX).
system allows to embed [/structural semantics](/research/structural-semantics) into
documents. Concretely sTeX is a "semantic version of LaTeX" that allows to use special
macros to encode mathematical meaning explicitly. This is (largely ignored in PDF
generation), but can be taken into account when generating [OMDoc-based](/systems/omdoc/) active documents.
## Resources
* [sTeX at GitHub](https://github.com/KWARC/sTeX) and the corresponding
[LaTeXML](http://dlmf.nist.gov/LaTeXML/)
[plugin for sTeX](https://github.com/KWARC/LaTeXML-Plugin-sTeX)
* Some sTeX-based libraries of active doucents on [MathHub.info](http://mathhub.info): [SMGloM](https://mathhub.info/smglom), [active course notes](https://mathhub.info/MiKoMH).
* Their sources can be found here: [SMGloM](https://gl.mathhub.info/smglom), [active course notes](https://gl.mathhub.info/MiKoMH).
## Documentation/Papers
* M. Kohlhase (2008) [*Using LaTeX as a semantic markup format*](https://kwarc.info/kohlhase/papers/mcs08-stex.pdf). Mathematics in Computer Science 2 (2), pp. 279–304
* ... [complete bibliography](http://kwarc.github.io/bibs/sTeX)
---
layout: system
menu_title: Semantic Alliance
title: Semantic Alliance
shorttitle: Sally
teaser: A framework for mashing up semantic services into desktop applications.
start_date: 2013-02
start_date: 2016-08
orphan: true
people:
- mkohlhase
- akohlhase
- cjucovschi
supported-by:
- sissi
- FormalCAD
logo: public/kwarc_logo.svg
repository: https://github.com/KWARC/Sally
people: mkohlhase,akohlhase,cjucovschi
publink: http://kwarc.github.io/bibs/sally
---
A distributed framework for mashing up semantic services into desktop applications.
---
layout: system
menu_title: SMGloM
title: "The Semantic, Multilingual Glossary of Mathematics"
pillar: KMR
start: 2013-11
people: mkohlhase,cjucovshi,miancu
title: "SMGLoM - A Semantic, Multilingual Glossary of Mathematics"
shorttitle: SMGLoM
teaser: A terminological resource for Mathematics
start_date: 2013-11
people:
- mkohlhase
- cjucovschi
- miancu
- twiesing
- jfschaefer
supported-by:
- mathsearch
- odk
logo: public/kwarc_logo.svg
publink: https://kwarc.github.io/bibs/smglom
---
The [Semantic, Multilingual Glossary of Mathematics](/systems/smglom/) is a
The SMGloM is a structured terminology for mathematics. It combines lexical information about the "Words of Mathematics" (in multiple languages) with semantic information about their dependencies. Multiple services can be derived from this terminology, e.g. a [classical glossary](https://mathhub.info/applications/glossary) and a [math dictionary](https://mathhub.info/applications/dictionary).
## Resources
* [SMGloM at MathHub.info](https://mathhub.info/library/group?id=smglom)
* [the SMGloM sources on gl.mathhub.info](https://gl.mathhub.info/smglom),
written in [sTeX](/systems/sTeX) (a semantic version of LaTeX)
* a [generated dictionary](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/dictionary.en-de-ro-zhs.pdf)
* various generated glossaries on the
[SMGloM applications repository](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/) for
[English](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.en.pdf),
[German](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.de.pdf),
[Chinese (simplified)](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.zhs.pdf),
[Romanian](https://gl.mathhub.info/smglom/meta-inf/tree/master/applications/glossary.ro.pdf)
## Papers
* D. Ginev, M. Iancu, C. Jucovshi, A. Kohlhase, M. Kohlhase, A. Oripov, J. Schefter, W. Sperber, O. Teschke and T. Wiesing (2016) [The SMGloM project and system: towards a terminology and ontology for mathematics](https://kwarc.info/kohlhase/papers/icms16-smglom.pdf) ICMS 2016
* M. Kohlhase (2014) [A data model and encoding for a semantic, multilingual terminology of mathematics](https://kwarc.info/kohlhase/papers/cicm14-smglom.pdf) CICM 2014
* [complete bibliography](https://kwarc.github.io/bibs/smglom/)
* [blue notes](https://gl.kwarc.info/smglom/blue): epsilon-baked ideas about how to continue
---
layout: system
menu_title: SWIM
title: "SWiM: Semantic Wiki for Mathematics"
start: 2006-08
end: 2009-06
people: mkohlhase,clange
shorttitle: SWiM
teaser: A Semantic Wiki for Interactive Mathematics.
start_date: 2006-08
end_date: 2009-06
publink: http://kwarc.github.io/bibs/swim
logo: public/kwarc_logo.svg
people:
- clange
- mkohlhase
---
SWIM is a Semantic Wiki for Interactive Mathematics. The system has been superseded by [MathHub](/systems/mathhub/).
---
layout: system
menu_title: TGView3D
shorttitle: TGView3D
title: The TGView3D Graph Viewer
teaser: An interactive 3D graph viewer optimized for visualizing Theory Graphs and mathematical knowledge in general
start_date: '2018'
people:
- mkohlhase
- frabe
- dmueller
- rmarcus
supported-by:
- odk
website: https://tgview3d.mathhub.info/
repository: https://github.com/UniFormal/tgview3d
publink: https://kwarc.info/people/mkohlhase/submit/cicm20-tgview3D.pdf
---
The TGView3D System is a 3D-theory graph viewer in the Unity Engine.
Different layouts and highlighting settings are available to visualize the complex theory graphs efficiently.
In particular, this allows exploration of big mathematical libraries, e.g, those related to theorem provers like Coq or Isabelle.
Furthermore, we have a virtual reality protoype to allow intuitive and immersive interactions.
*For students*: Topics for theses and projects are available [here](https://gl.kwarc.info/kwarc/thesis-projects/-/issues?label_name%5B%5D=Graph+Visualization).
\ No newline at end of file
---
layout: course
instructor: Prof. Dr. Michael Kohlhase
title: Projekt zur Künstlichen Intelligenz
menu_title: KI-Projekt
taught: WS16/17, SS16
---
The KWARC group (Wissensrepräsentation und Verarbeitung)conducts research in knowledge representation and reasoning techniques with a view towards applications in knowledge management.
We extend techniques from formal methods 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 in technical documents.
This level of markup allows for offering interesting knowledge management services without forcing theauthor to formalize the document contents.
In contrast to courses with fixed topics, project topics are defined individually.
See the [KWARC home page](http://kwarc.info) for a general introduction to the research and [the KWARC research topics list](http://gl.kwarc.info/kwarc/thesis-projects) for expemplary topics.
---
layout: course
instructor: Prof. Dr. Michael Kohlhase
title: Vorlesung *Logik-Basierte Wissensrepräsentation für Mathematisch/Technisches Wissen*
menu_title: Vorlesung KRMT
taught: SS16/17
---
Dieser Kurs behandelt Grundlagen der Mathematik, Modulare Formalisierung in
Theoriegraphen, Narrative Strukturen in informellen mathematisch/technischen Dokumenten,
Formalisierung von Logiksprachen in Metalogiken.
Da wir nur wenige Studenten erwarten, wollen wir diesen Kurs sehr interaktiv und
Projektorientiert aufbauen.
---
layout: course
instructor: Prof. Dr. Michael Kohlhase
title: Künstliche Intelligenz I
menu_title: Künstliche Intelligenz I
taught: WS16
---
Diese Vorlesung beschäftigt sich mit den Grundlagen der Künstlichen Intelligenz (KI), insbesondere formale Wissensrepräsentation, Heuristische Suche, Automatisches Planen und Schliessen unter Unsicherheit.