thesis-projects issueshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues2021-12-17T13:13:01Zhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/42Immersive Knowledge Interaction2021-12-17T13:13:01ZRichard MarcusImmersive Knowledge InteractionIn the FrameIT project (#1 and https://uframeit.github.io), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Currently...In the FrameIT project (#1 and https://uframeit.github.io), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Currently, the player can only interact with knowledge items via a special UI that mirrors the knowledge formalized in MMT as *scroll*. This 2D UI causes a cognitive dissonance to the 3D world that it talks about. A more immersive solution would fit better (at least for some applications)
For more immersion, we would like to
- a) automatically synchronize certain facts about the world dynamically (e.g. for moving objects)
- b) use in-game triggers to communicate with the logic engine
- c) have in-game interfaces to communicate with the logic engine
- d) allow players to directly assign objects somehow instead of using the corresponding generated icons
or build other features that result in more fluent gameplay.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/41Linking Formalized Situations to specific Game Objects/Situations2020-12-20T09:26:44ZRichard MarcusLinking Formalized Situations to specific Game Objects/SituationsIn the FrameIT project (#1), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Based on parametric situation theories, ...In the FrameIT project (#1), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Based on parametric situation theories, which are instantiated by "pretty small Unity scripts", we want to link the parameters to specific points in the world modeled in Unity.
Our goal here is to create a toolkit for game developers that allows them to integrate the formalized knowledge into the games in the form of modular elements that can linked to game objects.
Work Areas:
- 1. Making the formalized knowledge available to the Unity Editor itself (https://learn.unity.com/tutorial/editor-scripting#), which could enable interactions like this:
- list available fact types so that developers can select which gadgets can create these facts
- list available scrolls so that developers can build levels based on the problems defined in the scrolls
- 2. Scripting the generation of semantic game objects
- we could define certain object attributes on the knowledge side like "base_tree"
- if the developer assigns this attribute to an object in the game it should then be enhanced automatically: place it in a 90 degree angle to the ground, generate snapzones for root and top, configure colliders
- 3. Advanced Toolkit Interactions based on 1 and 2, e.g., if a Fact is connected to a Gadget, we know which Gadget should be used to create a certain fact for a solution
- 4: Building a graphical tool for this. Unity recently acquired [Bolt](https://assetstore.unity.com/packages/tools/visual-scripting/bolt-163802). Maybe it could be integrated into this, maybe we want/need our own editor, needs investigation.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/40Configure WissKI instances from symbolic metadata2020-11-24T09:32:20ZMichael Kohlhasemichael.kohlhase@fau.deConfigure WissKI instances from symbolic metadataAt the moment, the [WissKI](https://wiss-ki.eu) instances created by the [WissKI Distillery](https://wisski.agfd.fau.de) are very elementary. It would be good if the user could configure them to their needs and then have them automatical...At the moment, the [WissKI](https://wiss-ki.eu) instances created by the [WissKI Distillery](https://wisski.agfd.fau.de) are very elementary. It would be good if the user could configure them to their needs and then have them automatically pre-configured. This project has the following parts:
* determine configuration options and their values; examples are
* desired modules,
* theming
* data for the DSGVO pages (impressum and such)
* admins, users (for automated account creation)
* data testament (what happens after the project is over; see https://gitlab.cs.fau.de/AGFD/wisski/-/issues/24) and its documentation page.
* develop a JSON schema for storing the choices.
* develop a configuration dialog that guides users through the data collection process, documenting the options and previewing the consequences of the choices.
* develop a configuration process that implements the configuration in a new WissKI instance.
* (possibly) allow to change and re-configure the instance.Tom WiesingTom Wiesinghttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/30SUMO to OMDoc/MMT exporter.2020-12-08T09:04:14ZMichael Kohlhasemichael.kohlhase@fau.deSUMO to OMDoc/MMT exporter.The Suggested Upper Merged Ontology [SUMO](http://www.adampease.org/OP/) is an upper ontology that lightly formalizes common sense situations. It woucd be very nice to have a translator of SUMO into MMT Theories. For that we need
* A me...The Suggested Upper Merged Ontology [SUMO](http://www.adampease.org/OP/) is an upper ontology that lightly formalizes common sense situations. It woucd be very nice to have a translator of SUMO into MMT Theories. For that we need
* A meta-theory for the KIF (Knowledge Interface Format)
* a translator for the [SUMO data](https://github.com/ontologyportal/sumo) to OMDoc/MMT.
SUMO seems licenced mostly under GPL, so we are allowed to do this and even republish it on MathHub (as long as we keep the GPL).
This would be a good basis for JLogic.Max RappMax Rapphttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/29FrameNet to OMDoc/MMT exporter.2022-04-22T12:14:49ZMichael Kohlhasemichael.kohlhase@fau.deFrameNet to OMDoc/MMT exporter.[FrameNet](https://framenet.icsi.berkeley.edu) is a semantic linguistic resource that collects a set of common frames that can be used for understanding common sense situations. It woucd be very nice to have a translator of FrameNet into...[FrameNet](https://framenet.icsi.berkeley.edu) is a semantic linguistic resource that collects a set of common frames that can be used for understanding common sense situations. It woucd be very nice to have a translator of FrameNet into MMT Theories. For that we need
* A metatheory (FrameNetLogic)
* a translator for the FrameNet data, which comes as an XML file.
I have already requested the data.
FrameNet is licensed under Creative Commons Attribution, so we are allowed to do this and even republish it on MathHub (as long as we attribute).
This would be a good basis for JLogic.Frederik SchaeferFrederik Schaeferhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/28Build an integrated SPARQL index/endpoint for MathHub2020-07-30T11:25:15ZMichael Kohlhasemichael.kohlhase@fau.deBuild an integrated SPARQL index/endpoint for MathHubWe are slowly building up capacities for [tetrapodal search](https://kwarc.info/people/mkohlhase/papers/cicm20-search.pdf) in [MathHub](https://mathhub.info), i.e. search capacities across mathematical aspects.
For that we need an inde...We are slowly building up capacities for [tetrapodal search](https://kwarc.info/people/mkohlhase/papers/cicm20-search.pdf) in [MathHub](https://mathhub.info), i.e. search capacities across mathematical aspects.
For that we need an index for the *organizational aspect* which can mostly be expressed in terms of RDF graphs and queried via SPARQL. We already have quite a lot of data from our theory graphs and theorem prover libraries; see [the ULO paper](https://kwarc.info/kohlhase/papers/cicm19-ulo.pdf).
Now we need a dedicated index and query engine for them integrated into [MathHub](https://mathhub.info). I am thinking of [GraphDB](https://www.ontotext.com/products/graphdb/) a powerful system that is free in the basic tier. And give it a good test-drive with our data.Tom WiesingTom Wiesinghttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/27OEIS importer and extension for MathDataHub2020-12-08T09:05:50ZMichael Kohlhasemichael.kohlhase@fau.deOEIS importer and extension for MathDataHub[MathDataHub](http://data.mathhub.info) (MDH) is a deep FAIR system for mathematical data sets. Currently, it has mostly been used for systematic data sets like the [Small Groups Library](https://data.mathhub.info/collection/smallgp/).
...[MathDataHub](http://data.mathhub.info) (MDH) is a deep FAIR system for mathematical data sets. Currently, it has mostly been used for systematic data sets like the [Small Groups Library](https://data.mathhub.info/collection/smallgp/).
Having the [OEIS](http://oeis.org) (Encyclopedia of Integer Sequences) in [MathDataHub](http://data.mathhub.info) would be a major undertaking and a major success. Some of this we have already done, see [E. Luzhnica and M. Kohlhase (2016) Formula semantification and automated relation finding in the OEIS. ICMS 2016](http://kwarc.info/kohlhase/papers/icms16-oeis.pdf). This needs to be made sustainable and much more complete. [MathDataHub](http://data.mathhub.info) and [MathHub](http://mathhub.info) are the right tools/targets for this. We have to
* get our hands on the OEIS dumps - KWARC has the necessary contacts - and build an infrastructure to keep the content synced.
* build a parser for the OEIS that is as lossless as possible
* formalize the meta-theory of OEIS in MMT.
* Build the MDDL Schema theories for the OEIS
* (optionally) Build specialized User Interfaces on top of MDH.
* (optionally) build a programmatic API for the OEIS.
Clearly this is a project for a whole group, and the later points are optional.
One of the high proints of this project is that there is a good chance that there will be funding (and possibly future employment options via the [NFDI](https://de.wikipedia.org/wiki/Nationale_Forschungsdateninfrastruktur) KWARC is part of the [MaRDI Consortium](http://wias-berlin.de/mardi/).Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/8Theory Graph Visualization and Interaction Front-End2020-05-01T23:34:39ZMichael Kohlhasemichael.kohlhase@fau.deTheory Graph Visualization and Interaction Front-EndThe central data structure of the OMDoc/MMT format and system is that of a theory graph, where nodes are theories and the edges are theory morphisms, (or alignments, see #7). We extensively use this structure in all of our services, but ...The central data structure of the OMDoc/MMT format and system is that of a theory graph, where nodes are theories and the edges are theory morphisms, (or alignments, see #7). We extensively use this structure in all of our services, but only have very limited means of actually seeing them and interacting with them (we currently generate static SVG presentations via graphviz.
The topic here is to build a client-side (i.e. in-browser) graph interface based on a javascript ligrary for graph layout and interaction (most probably [vis.js network](http://visjs.org). This interface should support
* interactive graph visualization: showing/hiding parts of a graph, highlighting certain features, clustering, ...
* inspection of theories and edges (by clicking on them)
* addition/deletion/update of nodes and edges (e.g. for alignments)
* graph export for didactic purposes.
* ... I am sure more ideas will pop up when we play with this ...Dennis MüllerDennis Müllerhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/2Spotting and Searching Quantity Expressions technical/scientific documents (t...2018-02-07T14:28:44ZMichael Kohlhasemichael.kohlhase@fau.deSpotting and Searching Quantity Expressions technical/scientific documents (towards a physics search engine)KWARC group has converted the [Cornell EPrint arXiv](http://arxiv.org) (> 1.1 Million papers in physics, maths, CS, etc) into HTML5. This resource contains millions of quantity expressions like "3m/s" , "13 square mile feet", or "five as...KWARC group has converted the [Cornell EPrint arXiv](http://arxiv.org) (> 1.1 Million papers in physics, maths, CS, etc) into HTML5. This resource contains millions of quantity expressions like "3m/s" , "13 square mile feet", or "five astronomical units". One step towards a "physics search engine" would be to make those searchable as quantity expressions, i.e. if we could find "3m/s" by searching for "10.8 km/h" or "?x furlongs per fortnight" - independently of the unit used to represent the quantity. We have most of the parts needed for such a search engine; here is what would be needed to build it:
* build a spotter for quantity expressions for deployment in [CorTeX](http://cortex.mathweb.org)
cc: @dmueller @miancuMichael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.de