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
Hide whitespace changes
Inline Side-by-side
Showing
with 238 additions and 127 deletions
public/pubs.jpg 0 → 100644
View file @ 638ce3bc
public/pubs.jpg

21.3 KiB

public/researchgate.jpg 0 → 100644
View file @ 638ce3bc
public/researchgate.jpg

11.3 KiB

public/www.jpg 0 → 100644
View file @ 638ce3bc
public/www.jpg

15.4 KiB

public/zbmath.png 0 → 100644
View file @ 638ce3bc
public/zbmath.png

7.01 KiB

research/formal-methods.md
View file @ 638ce3bc
......@@ -4,12 +4,19 @@ title: Formal Methods
menu_title: Formal Methods
menu_order: 102
---
## Formal Methods
This term usually identifies a set of technologies that presuppose representing the objects involved in some kind of logic with a well-defined semantics. The term formal refers to the fact that any action on the objects can be based on their form only. This usually means that the representations are quite elaborate and can be tedious to work with for humans, but also that these actions can be performed by machines.
This term usually identifies a set of technologies that presuppose representing the objects involved in some kind of logic with a well-defined semantics. The term ``formal`` refers to the fact that any action on the objects can be based on their form only. This usually means that the representations are quite elaborate and can be tedious to work with for humans, but also that these actions can be performed by machines.
Therefore formal methods are highly successful in applications where a high degree of confidence is desired, e.g. in program verification, as the foundation of mathematics, or even in legal frameworks. To accommodate for these applications a large zoo of logics has been developed and mechanized reasoning systems have been developed.
## In a little more detail
#### Entailment Systems
The foundation of formal methods is the entailment relation ⊧, a relation between a set Φ of formulae (the assumptions) and a formula T : Φ ⊧ T signifies that T must be true in all situations, where the assumptions in Φ are. So, if Φ is empty, T must be true in all situations, and we call it a theorem. The relation ⊧ is usually defined by reference to some externally given semantics, but can be approximated by a calculus. This gives the notion of a proof: we know Φ ⊧ T , if there is a proof of T from Φ that conforms to the rules of the calculus. So Φ ⊧ T can be verified by purely syntactical means, giving us a way to establish theorem-hood by a machine.
#### Logical Systems
Entailment systems usually induced by logics, i.e. formal languages for representing knowledge with a model and/or proof theory. The KWARC group develops meta-logical approaches for modeling logics and the relations between them. For instance, we have developed the [LATIN Logic Atlas](/projects/latin/); a graph of more than 1000 logic fragments and logic-translations.
#### Interoperability in Formal Methods
There are literally hundreds of formal systems for representing, reasoning about, and computing with STEM knowledge. The KWARC group is developing a general, knowledge-based interoperability architecture: the Math-in-the-Middle (MitM) Approach to interoperability. We use modularly represented mathematical knowledge as a pivot point for connecting systems. In the [OpenDreamKit](/projects/odk) we instantiate this for computer algebra systems, and in the [OAF](/projects/oaf) for theorem prover (libraries).
research/index.md 0 → 100644
View file @ 638ce3bc
---
layout: page
title: KWARC Research
menu_title: Overview
hidden: true
---
The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management.
We extend techniques from [formal methods](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](structural-semantics/) in technical documents.
This level of markup allows for offering interesting [knowledge management services](kminteract/) without forcing the author to fully formalize the document contents, we are working on methods for [semi-automated semantization](semantization/).
All in all, the research in the KWARC group is summarized in the schema below, which can be read as a pipeline from foundations (on the bottom) to applications (on the top).
<table style="border: 1px solid black">
<col width="33%"/>
<col width="33%"/>
<col width="33%"/>
<tbody>
<tr style="border: 1px solid black">
<td colspan="3">
<span style="font-weight:bold">Applications</span>
eMath 3.0,
<a href="https://mathhub.info">Active Documents</a>,
<a href="/projects/SiSsI/">Semantic Spreadsheets</a>,
<a href="/projects/FormalCAD/">Semantic CAD/CAM</a>,
Semantic Help Systems, Change Mangagement, ...
</td>
</tr>
<tr>
<td style="border: 1px solid black">
<span style="font-weight:bold">Foundations of Mathematics</span>
<ul>
<li><a href="https://omdoc.org">OMDoc</a></li>
<li><a href="http://uniformal.github.io">MMT: Modular Math Theories</a></li>
<li><a href="/projects/latin">Logic Morphisms/Atlas</a></li>
<li>Advanced Type Theories</li>
<li><a href="/projects/oaf/">Theorem Prover</a> and <a href="../projects/odk/">Computer Algebra</a> Interoperability</li>
</ul>
</td>
<td style="border: 1px solid black">
<a href="kminteract"><span style="font-weight:bold">Knowledge Mgt. &amp; Interaction</span></a>
<ul>
<li>Semantic Interpretation</li>
<li><a href="/systems/mws/">Math Web Search</a></li>
<li><a href="/systems/mathhub/">MathHub</a></li>
<li><a href="/systems/frameit/">Serious Games</a></li>
</ul>
</td>
<td style="border: 1px solid black">
<a href="semantization">
<span style="font-weight:bold">Semantization</span>
</a>
<ul>
<li><a href="/projects/arXMLiv/">LaTeX --&gt; XML</a></li>
<li><a href="/systems/sTeX/">sTeX: Semantic LaTeX</a></li>
<li>Context-Aware IDEs</li>
<li>Mathematical <a href="http://gl.mathhub.info">Corpora</a> and <a href="sigmathling.kwarc.info">data sets</a></li>
<li><a href="/projects/comma/">Linguistics of Math</a></li>
</ul>
</td>
</tr>
<tr style="border: 1px solid black">
<td colspan="3">
<span style="font-weight:bold">Foundations:</span>
Computational Logic,
<a href="formal-methods/">Formal Methods</a>,
<a href="http://www.w3.org/TR/MathML3/">MathML</a>,
<a href="http://openmath.org">OpenMath</a>
</td>
</tr>
</tbody>
</table>
The KWARC Group welcomes student involvement in research. If you are interested, please send an e-mail to <michael.kohlhase@fau.de>, or come to our seminars and courses
We have an initial list topics for [theses, or guided research](https://gl.kwarc.info/kwarc/thesis-projects)
research/kminteract.md
View file @ 638ce3bc
---
layout: page
title: Knowledge Management & Interaction
menu_title: KM & Interaction
title: Semantic Services, Knowledge Management & Interaction
menu_title: Services, KM & Interaction
menu_order: 104
---
...more to be written ...
The purpose of [knowledge representation](structural-semantics/) and
[formalization](formal-methods/) is the provisioning of semantic services and ways of
interacting with the represented knowledge that would be impossible if the knowledge
structures were still implicity, - i.e. before [semanitzation](semantization/).
The KWARC group develops various semantic services and ways of interacting with the
underlying semantics of documents. For instance, the
research/overview.md deleted 100644 → 0
View file @ b206c24f
---
layout: page
title: KWARC Research
menu_title: Overview
menu_order: 101
---
The KWARC research group conducts research in knowledge representation with a view towards applications in knowledge management. We extend techniques from [formal methods](http://kwarc.info/research/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](http://kwarc.info/structural-semantics) in technical documents. This level of markup allows for offering interesting [knowledge management services](http://kwarc.info/research/kminteract/) without forcing the author to fully formalize the document contents, we are working on methods for [semi-automated semantization](http://kwarc.info/research/semantization/). All in all, the research in the KWARC group is summarized in the schema below, which can be read as a pipeline from foundations (on the bottom) to applications (on the top).
<table>
<tbody>
<tr>
<td colspan="3">
<span style="font-weight:bold">Applications</span>
eMath 3.0,
<a href="https://planetary.mathweb.org">Active Documents</a>,
<a href="https://trac.kwarc.info/sissi">Semantic Spreadsheets</a>,
<a href="https://trac.kwarc.info/FormalCAD">Semantic CAD/CAM</a>,
Semantic Help Systems, Change Mangagement, ...
</td>
</tr>
<tr>
<td>
<span style="font-weight:bold">Foundations of Mathematics</span>
<ul>
<li><a href="https://omdoc.org">OMDoc</a></li>
<li>advanced Type Theories</li>
<li><a href="http://uniformal.github.io">MMT: Modular Math Theories</a></li>
<li><a href="http://trac.omodoc.org/LATIN">Logic Morphisms/Atlas</a></li>
<li>Theorem Prover Interoperability</li>
</ul>
</td>
<td>
<a href="http://kwarc.info/research/kminteract"><span style="font-weight:bold">Knowledge Mgt. &amp; Interaction</span></a>
<ul>
<li>Semantic Interpretation</li>
<li><a href="https://trac.omdoc.org/JOBAD">JOBAD: Document-Embedded Interaction</a></li>
<li><a href="https://trac.mathweb.org/tntbase">TNTBase: Versioned XML Storage</a></li>
<li><a href="http://trac.mathweb.org/MWS">Math Web Search</a></li>
<li>Math Archives</li>
</ul>
</td>
<td>
<a href="http://kwarc.info/research/semantization">
<span style="font-weight:bold">Semantization</span>
</a>
<ul>
<li><a href="http://github.com/brucemiller/LaTeXML">LaTeX --&gt; XML</a></li>
<li><a href="http://github.com/KWARC/sTeX">sTeX: Semantic LaTeX</a></li>
<li>invasive editors</li>
<li>Context-Aware IDEs</li>
<li>Mathematical Corpora</li>
<li><a href="https://github.com/KWARC/llamapun">Linguistics of Math</a></li>
</ul>
</td>
</tr>
<tr>
<td colspan="3">
<span style="font-weight:bold">Foundations:</span>
Computational Logic,
<a href="/formal-methods">Formal Methods</a>,
<a href="http://www.w3.org/TR/MathML3/">MathML</a>,
<a href="http://openmath.org">OpenMath</a>
</td>
</tr>
</tbody>
</table>
research/semantization.md
View file @ 638ce3bc
......@@ -4,4 +4,22 @@ title: Semi-Automated Semantization
menu_title: Semantization
menu_order: 105
---
...more to be written ...
is the process of making the knowledge and structure in informal representations explicit,
so that they can be acted upon by machines.
Currently, 99% of the available mathematical kwnoledge is encoded in informal mathematical
documents: journal articles, books, preprints, handwritten course notes or recordings of
lectures. To make these accessible to
[semantic services and knowledge managment systems](kminteract), we must semanticize them.
The KWARC group engages in multiple projects to help along semantization. In the
[sTeX](/systems/sTeX/) format, we enable authors to semantically prelaop LaTeX documents
so that we can generate [OMDoc](/systems/OMDoc) representation from them (again via
[LaTeXML](http://dlmf.nist.gov/LaTeXML)).
In the [arXMLiv project](/systems/arXMLiv) we transform the
[Cornell ePrint arXiv](http://arxiv.org) into XML with MathML and explicit document
structure via [LaTeXML](http://dlmf.nist.gov/LaTeXML). In the [LLaMaPuN](/systems/lamapun)
project we develop libraries for automatically identifying meaning structures in arXMLiv
documents so that we will eventually be able to harvest OMDoc from the results.
research/structural-semantics.md
View file @ 638ce3bc
......@@ -3,6 +3,11 @@ layout: page
title: Structural Semantics
menu_order: 103
---
Computer support for document interaction is only possible, if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with formal methods. In many cases, useful services can be rendered by machines without having an entailment relation, for instance we can search for a formula, we can determine the concepts it depends upon, etc. The commonality of such services is that they are based on the structure of the formulae alone. For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
...more to be written ...
Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with [formal methods](../formal-methods/).
In many cases, useful [mathematical services](../kminteract/) can be rendered by machines without having an [entailment relation](../formal-methods/), for instance we can search for a formula, we can determine the concepts it depends upon, etc.
The commonality of such services is that they are based on the structure of the formulae alone.
For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof.
We speak of *structural semantics* as a lightweight form of meaning annotation.
So instead of formalizing mathematical knowledge to a level where an entailment relation can be induced, we can use structural descriptions instead, e.g. by annotating certain properties to mathematical documents turning them into [objects of flexible formality](https://mathhub.info/help/FlexiForms.html).
run 0 → 100755
View file @ 638ce3bc
bundle exec jekyll serve
students/index.md deleted 100644 → 0
View file @ b206c24f
---
layout: page
title: For Students
menu_title: KWARC For Students
menu_order: 101
---
The KWARC Group welcomes student involvement in research. If you are interested, please send an e-mail to <michael.kohlhase@fau.de>, or come to our seminars and courses
We have an initial list topics for [theses, or guided research](https://gl.kwarc.info/kwarc/thesis-projects)
systems/TNTBase.md
View file @ 638ce3bc
---
layout: system
title: TNTBase
shorttitle: TNTBase
teaser: A Versioned Storage for Mathematics (OMDoc)
start: 2009-09
end: 2012-08
people: mkohlhase,vzholudev
start_date: 2009-09
end_date: 2012-08
people:
- mkohlhase
- vzholudev
logo: public/kwarc_logo.svg
publink: http://kwarc.github.io/bibs/tntbase
---
TNTBase is a database which is optimized for storing mathematical documents in OMDoc format. It is based on Subversion and Berkeley DB XML.
systems/active.md deleted 100644 → 0
View file @ b206c24f
---
layout: default
title: Active Systems
menu_title: Active
menu_order: 100
---
## Actively Developed Systems ([Historic Systems](/systems/historic))
listing to be generated here.
systems/arXMLiv.md deleted 100644 → 0
View file @ b206c24f
---
layout: system
title: arXMLiv
start: 2006
pillar: semantization
people: mkohlhase,dginev
---
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 to have a basis for uncovering it's structural semantics.
systems/cpoint.md
View file @ 638ce3bc
---
layout: system
title: CPoint
shorttitle: CPoint
teaser: Adding a semantic layer to MS PowerPoint.
start: 2001-07
end: 2008-04
people: akohlhase
start_date: 2001-07
end_date: 2008-04
people:
- akohlhase
publink: http://kwarc.github.io/bibs/cpoint
logo: public/kwarc_logo.svg
---
CPoint is an extension to MS PowerPoint that allows to add and manage semantic annotations
in PowerPoint presentations. The system offers various embedded semantic services.
systems/frameit.md 0 → 100644
View file @ 638ce3bc
---
layout: system
menu_title: FrameIt
shorttitle: FrameIT
title: The UFrameIT Framework
teaser: A Framework for Serious Games by combining Virtual Worlds with Mathematical Knowledge Management
start_date: '2013'
people:
- mkohlhase
- dmueller
- rmarcus
- nroux
- jschihada
supported-by:
- oaf
website: https://uframeit.org
repository: https://github.com/UFrameIT
publink: http://kwarc.github.io/bibs/frameit
---
The FrameIT project builds a Framework for Serious Games by combining Virtual Worlds with
Mathematical Knowledge Management. The main idea is that we can use
[MMT](https://kwarc.info/projects/mmt) theory graphs to represent the background knowledge
and [MMT](https://kwarc.info/projects/mmt) pushouts to compute the application of
knowledge in concrete situations.
The [UFrameIT](https://github.com/UFrameIT) framework uses the
[Unity game engine](http://unity.com) with the [MMT](https://kwarc.info/projects/mmt)
system.
*For students*: Topics for theses and projects are available [here](https://gl.kwarc.info/kwarc/thesis-projects/-/issues?label_name%5B%5D=FrameIT).
systems/jobad.md 0 → 100644
View file @ 638ce3bc
---
layout: system
title: JOBAD
shorttitle: JOBAD
teaser: A Javascrip Framework for instrumenting Active Documents with Semantic Services
start_date: 2008-09
end_date: 2015-12
oprhan: true
people:
- frabe
- twiesing
logo: public/kwarc_logo.svg
publink: http://kwarc.github.io/bibs/jobad
repository: https://github.com/kwarc/jobad
---
JOBAD (JavaScript API for OMDoc-based Active Documents) is a javascript framework which
makes it easy to create interactive web pages.
systems/jomdoc.md
View file @ 638ce3bc
---
layout: system
title: JOMDoc
teaser: A Java API for OMDoc documents.
start: 2007-09
end: 2013-12
people: mkohlhase,nmueller
shorttitle: JOMDoc
teaser: A Java API for OMDoc documents
start_date: 2007-09
end_date: 2013-12
people:
- mkohlhase
- nmueller
logo: public/kwarc_logo.svg
---
JOMDoc is Java API for OMDoc documents that facilitates the parsing of OMDoc XML documents into a Java data structure, to manipulate them conveniently, and to serialize the result back to XML. The functionality of this library will be superseded by the MMT API in the near future.
systems/kat.md
View file @ 638ce3bc
---
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.