thesis-projects issueshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues2020-05-01T23:34:36Zhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/363D Theory Graph Visualization2020-05-01T23:34:36ZRichard Marcus3D Theory Graph VisualizationAs a follow up to #8, we have developed an interactive [3D graph viewer](https://github.com/UniFormal/tgview3d).
Based on this, there are several possibilities for further research:
- extending the virtual reality prototype with state-of...As a follow up to #8, we have developed an interactive [3D graph viewer](https://github.com/UniFormal/tgview3d).
Based on this, there are several possibilities for further research:
- extending the virtual reality prototype with state-of-the-art interaction concepts
- developing library-specific, specialized builds
- comparing different layout algorithms
- optimizing layout computationMichael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/25Intellij support for MMT-jupyter-notebooks2020-01-03T09:11:22ZDennis MüllerIntellij support for MMT-jupyter-notebooksSee https://github.com/UniFormal/IntelliJ-MMT/issues/28See https://github.com/UniFormal/IntelliJ-MMT/issues/28https://gl.kwarc.info/kwarc/thesis-projects/-/issues/21Data Dimension for MathHub.info2018-07-25T00:03:43ZMichael Kohlhasemichael.kohlhase@fau.deData Dimension for MathHub.infoThe [MathHub.info](http://mathhub.info) system currently only has active/semantic documents and theory graphs. But we would like to integrate and host mathematical data bases like the [OEIS](http://oeis.org) or [LMFDB](http://lmfdb.org) ...The [MathHub.info](http://mathhub.info) system currently only has active/semantic documents and theory graphs. But we would like to integrate and host mathematical data bases like the [OEIS](http://oeis.org) or [LMFDB](http://lmfdb.org) with mathematical interfaces.
The theory and part of the implementation has already been done in [virtual theories](https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/MACIS17-vt/crc.pdf) and is proposed as part of #20. Now we need to build the infrastruture in [MathHub.info](http://mathhub.info). Concretely, this involves
* installing and exposing a data base server as <http://data.mathhub.info> (probably Postgres or so)
* extending the MMT `lmh` extension to create data bases for any archive with virtual theories (i.e. theories for which the necessary codecs and schema theories exist)
* developing a process for syncing the access permissions in the data base with those for the archive at http://gl.mathhub.info
* develop a MMT `data` extension with a structure component that creates/updates tables for MMT theories and whose object component uses queries for MMT expressions.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/18Integrate Kwarc tools with GitLab2018-05-17T13:20:01ZFlorian RabeIntegrate Kwarc tools with GitLabGitLab is a major open-source locally-installable GitHub-style git repository manager.
The Kwarc uses it as the backend of our MathHub system. See [https://gl.mathhub.info/users/sign_in](https://gl.mathhub.info/users/sign_in).
GitLab is...GitLab is a major open-source locally-installable GitHub-style git repository manager.
The Kwarc uses it as the backend of our MathHub system. See [https://gl.mathhub.info/users/sign_in](https://gl.mathhub.info/users/sign_in).
GitLab is mostly monolithic, but like any open-source toll it must offer some interface to customize it.
In this project, a student
* peruses GitLab for such options
* identifies potential for integrating Kwarc knowledge management solutions with it
* designs and implements these integrations
Examples and starting points:
* GitLab uses some general purpose syntax highlighting framework.
But currently our .mmt files are rendered as plain text.
Find out which framework GitLab uses, write a syntax highlighter for .mmt files in it, and configure GitLab to use it.
* GitLab provides a very simple plugin interface for event handling.
Write an even handler that scans every new issue for special annotations that tie individual issues to MMT URIs.
Then customize MMT-based tools to display links to these issues, e.g., jEdit can display button whenever an issue for a declaration exists.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/17applications of viewfinding2018-05-15T06:02:08ZMichael Kohlhasemichael.kohlhase@fau.deapplications of viewfinding@dmueller has recently implemented a viewfinder, i.e. a function that finds MMT views (and partial ones as well) in an OMDoc/MMT library or between more than one. This [paper](http://kwarc.info/kohlhase/submit/cicm18-viewfinder.pdf) des...@dmueller has recently implemented a viewfinder, i.e. a function that finds MMT views (and partial ones as well) in an OMDoc/MMT library or between more than one. This [paper](http://kwarc.info/kohlhase/submit/cicm18-viewfinder.pdf) describes the specifics and lists a bunch of applications in the back. The project is to implement one or more of these applications in [MathHub](https://mathhub.info).
The necessary steps are
* fully understand viewfinding and the intended application
* build an extended example and produce the mathematical resources
* specify the context of use and the user interactdions
* build a front-end that supports these.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/16implementing Realms as an MMT structural feature2018-02-07T14:41:37ZMichael Kohlhasemichael.kohlhase@fau.deimplementing Realms as an MMT structural featureWe have this global language feature of realms, see http://kwarc.info/kohlhase/papers/cicm14-realms.pdf and http://kwarc.info/kohlhase/papers/cicm15-induced.pdf and http://kwarc.info/kohlhase/papers/cicm15-recaps.pdf This is a very well-...We have this global language feature of realms, see http://kwarc.info/kohlhase/papers/cicm14-realms.pdf and http://kwarc.info/kohlhase/papers/cicm15-induced.pdf and http://kwarc.info/kohlhase/papers/cicm15-recaps.pdf This is a very well-understood practical device that makes theory graphs much closer to mathematical practice.
This needs to be implemented in MMT (following and building on Mihnea Iancu's thesis), and a management interface needs to be designed. And of course tested on the examples Mihnea and I have designed. Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/15program persistence layer in MathDataHub2021-02-22T15:44:24ZMichael Kohlhasemichael.kohlhase@fau.deprogram persistence layer in MathDataHubIn the [OpenDreamKit project](https://opendreamkit.org) our colleagues developed the pypersist package that allows programmers to (easily) make their results persistent. We should have a more semantic version of this as part of MathDataH...In the [OpenDreamKit project](https://opendreamkit.org) our colleagues developed the pypersist package that allows programmers to (easily) make their results persistent. We should have a more semantic version of this as part of MathDataHub, so we can get at interesting data and index them.
An example is a polynomial *factorization service (with caching)* This is a service that just caches factorizations and looks them up. Details at https://github.com/KWARC/mws/issues/102
I really think that (if done right) this would have quite an impact.
But the general project is much greater.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/13Implement Lenses/States for MathHub2018-11-24T09:41:32ZMichael Kohlhasemichael.kohlhase@fau.deImplement Lenses/States for MathHubWe would like to have an infrastructyure quality control in MathHub. The model that seems adequate is the "lenses" model introduced by the [connexions project; now OpenStax](http://cnx.org). The idea is to allow open submission to MathHu...We would like to have an infrastructyure quality control in MathHub. The model that seems adequate is the "lenses" model introduced by the [connexions project; now OpenStax](http://cnx.org). The idea is to allow open submission to MathHub and do the quality control later by allowing anyone to define a named "lens", which endorses certain objects as "interesting and (sufficiently) good" and which can be used by users to direct their attention.
The important innovation is that lenses are public and can be created, followed, copied & extended by anyone. Communities will usually have their own "quality approved" lens, and lenses can also be used as an "overlay journal" over MathHub.
Some details of the idea are in this [blue note](https://gl.kwarc.info/smglom/blue/tree/master/contmgt/note.pdf), and there is a recent [MathHub issue](https://github.com/MathHubInfo/Frontend/issues/88) that goes more into detail about implementation. https://gl.kwarc.info/kwarc/thesis-projects/-/issues/12Theory Graph Minimization2017-07-31T19:36:29ZMichael Kohlhasemichael.kohlhase@fau.deTheory Graph MinimizationKWARC develops and imports theory graphs for mathematical knowledge. A theory consists of of symbols and declarations (statements that describe the properties and interactions of symbols). For an "object-oriented" development we use spec...KWARC develops and imports theory graphs for mathematical knowledge. A theory consists of of symbols and declarations (statements that describe the properties and interactions of symbols). For an "object-oriented" development we use special declarations: inclusions and structures that import other theories (symbol/declaration inheritance). Furthermore theories can be connected by special truth-preserving mappings: views.
In practice (especially when curating theory graphs) it often happens that the inclusions, structures, and views are not minimal: We call an inclusion A includes B minimal, iff there is no theory C, such that including C in A would give the same result (details more complicated, but rather straightforward). Minimality of other theory graph components is similar, and a theory graph is minimal, iff all its components are.
Theoretically, non-minimal theory graphs are not a problem, but minimizing them maximizes the induced knowledge space (more theorems are induced). Furthermore practically, minimal theory graphs are easier to deal with (e.g. inclusions and views form a transitive skeleton, which reduces edge clutter, which can be fatal in large graphs).
For bigger theory graphs, minimality is not trivial (and very tedious) for humans to determine, so we would like a tool to support this. This minimality would be implemented in the [MMT API](http://uniformal.github.io) (i.e. in Scala) and would propose changes that make the graph minimal. These could be delivered as a patch to the surface symatx of the theory graph (i.g. [MMT native syntax](http://uniformal.github.io) or [sTeX](https://github.com/KWARC/sTeX), which can directly be applied (e.g. in an interactive text-based tool that can be integrated into an editor) or in the form of a pull request on http://gl.mathhub.info (where the theory graphs live).Dennis MüllerDennis Müllerhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/9Active Course notes2017-07-31T19:36:30ZMichael Kohlhasemichael.kohlhase@fau.deActive Course notesAll of Michael's teaching materials are marked up semantically in [sTeX](https://github.com/KWARC/sTeX), which can be transformed into OMDoc/iMMT-based **active documents**, which have embedded semantic services e.g.
* **guided tours**...All of Michael's teaching materials are marked up semantically in [sTeX](https://github.com/KWARC/sTeX), which can be transformed into OMDoc/iMMT-based **active documents**, which have embedded semantic services e.g.
* **guided tours** (generated mini-courses that explain a particular concept in the document)
* **definition lookup** (click on a word or symbol in a formula and get a popup with the definition)
* **technical dictionary** find the German words for technical terms in the English slides.
* **user modelling**: the system monitors your progress of understanding the material and adapts its services (e.g. the guided tours do not show you things you already know).
* **pop-quiz** where you can show (the user model) that you understood things.
We have the basic technology to do this, but this needs to be revisited to actually make this into a tool that students can use.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/7Finding and Presenting Alignments in Math Libraries2017-07-31T19:36:30ZMichael Kohlhasemichael.kohlhase@fau.deFinding and Presenting Alignments in Math LibrariesWe importer formal and informal libraries of mathematics into the [MathHub](http://mathhub.info) system. The formal libraries are mostly theorem prover libraries (Mizar, HOL Light, Isabelle, IMPS, PVS, ... ) and the informal ones are bas...We importer formal and informal libraries of mathematics into the [MathHub](http://mathhub.info) system. The formal libraries are mostly theorem prover libraries (Mizar, HOL Light, Isabelle, IMPS, PVS, ... ) and the informal ones are based on annotated LaTeX.
We observe that there is quite a lot of overlap between the libraries, and we have developed a notion of "alignments" (see a [recent paper](http://kwarc.info/kohlhase/submit/alignments16.pdf) and have collected an [initial set](https://gl.mathhub.info/alignments/Public).
This general topic has various sub-projects that can be tackled individually or together
1. building an alignment navigator/interface, which allows users to get an overview over the overlap and how concepts relate (Akbar Oripov is working on this at Jacobs University).
2. manually finding complex alignments and categorizing them, and building a curation system for that.
3. building software that goes over the libraries and suggests alignments of various categories (to be curated in the system above).Dennis MüllerDennis Müllerhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/6Semantics extraction for assistive tools for scientists with disabilities (Ba...2017-07-31T19:36:30ZMichael Kohlhasemichael.kohlhase@fau.deSemantics extraction for assistive tools for scientists with disabilities (Bachelor or Master)There is a study that about 9% of the internet users have disabilities that make reading difficult (blindness, dyslexia, ...). For regular web pages, books, etc. there are assistive technologies like screen readers like Jaws (Windows) or...There is a study that about 9% of the internet users have disabilities that make reading difficult (blindness, dyslexia, ...). For regular web pages, books, etc. there are assistive technologies like screen readers like Jaws (Windows) or voiceover. Recently, these have acquired functionality to deal with MathML (e.g. MathML3 is now part of the DAISY and ARIA standards).
But the functionality is only as good as the input ("junk-in->junk-out" principle), so a formula like $X^{1/2}$ reads as "X upper index 1 slash 2" in e.g. JAWS instead of "X to the power of one half" (or even "square root of X").
If we had a system for semantics extraction (see #2 for an example) we could generate better input for screen readers and annotate it into the documents. Semantics extraction + integration into screen readers is a topic that could be in part (Bachelor) or fully (Master) tackled in a thesis.
We have excellent contacts into the assistive technologies community that would lead to real-world deployments and thus real-world impact.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.de