thesis-projects issueshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues2018-05-15T06:02:08Zhttps://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/14semantics extractions based on machine learning2017-04-13T08:05:33ZMichael Kohlhasemichael.kohlhase@fau.desemantics extractions based on machine learningWe have a couple of corpora from which we want to extract semantical features.
Examples are
* quantity expressions like "3m/s" (three meters per second) or "two furlongs per fortnight"
* polarity of identifiers in formulae (essential...We have a couple of corpora from which we want to extract semantical features.
Examples are
* quantity expressions like "3m/s" (three meters per second) or "two furlongs per fortnight"
* polarity of identifiers in formulae (essentially, which symbols in a formula can be substituted for)
* where are "definitions/theorems/assumptions" (and what are their definienda, definienses, and statemnets).
* or more generally what is the content form of a formula
If we know any of those, we could extend nice semantic features (e.g. better screen readers for visually challenged people or better scientific search engines) relatively directly.
We have a couple of large corpora e.g. the [arXMLiv corpus](cortex.mathweb.org/corpus/arXMLiv/tex_to_html) or the data behind the [Online Encyclopaedia of Integer Sequences](http://oeis.org)
All of them are (probably) amenable to machine-learning methods. In some cases, we already have some data about the phenomena above which can act as a baseline.
The topic is to pick one or more of these aspects of semantics and see what contemporary statistical AI methods can do to scale these up to corpus size and develop an symbolic application (possibly with a lot of help from the group).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/11Theory Exploration2021-10-21T16:01:27ZFlorian RabeTheory ExplorationBy now MMT is strong enough to generate values of arbitrary types and compute with them.
This can be used for a generic theory exploration algorithm: Generate a formula, generate some values, test the formula.
If the formula is true for...By now MMT is strong enough to generate values of arbitrary types and compute with them.
This can be used for a generic theory exploration algorithm: Generate a formula, generate some values, test the formula.
If the formula is true for all values, it may be a theorem and is marked as such.
Later a human or a theorem can inspect the generated theorems and add the proofs.
----
For example, consider addition on the natural numbers with +, 0, and =.
MMT can generate formulas by
* using some (e.g., up to 3) free variables x,y,z
* systematically generate well-typed terms from them such as x, y, z, x+y, y+x, x+z, z+x, x+z, y+z, z+y, x+0, 0+x, and so on
* systematically generate values of N such as 0, 1, 3, 10, 13
* plug in all combinations of the values for x, y, z into the generated terms
* whenever two terms t(x,y,z) and t'(x,y,z) that agree on all values and conjecture the theorem forall xy.t(x,y,z)=t'(x,y,z)
Many important theorems can be guessed in this way, and for not-well-understood-yet theories, it's plausible that will include some new theorems.
----
There is already prior work on conjecture generation, historically by Simon Colton (look it up) and more recently by Josef Urban, Cezary Kaliszyck. The latter is quite compatible with this idea but is on different corpora.Florian RabeFlorian Rabehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/10Interactive Examples2021-10-21T16:01:32ZFlorian RabeInteractive ExamplesAdd a language feature (by implementing the class StructureFeature) for examples with free parameters.
To check or elaborate an example, nothing has to be done.
But the HTMLPresenter must be adapted to display examples nicely.
The exam...Add a language feature (by implementing the class StructureFeature) for examples with free parameters.
To check or elaborate an example, nothing has to be done.
But the HTMLPresenter must be adapted to display examples nicely.
The examples should be interactive: The user should be able to interactively enter values (in HTML text fields) for the parameters.
Then MMT could be called to recompute the example.
-----
We might have
"
Example (addition):
For every a,b, we have that a+b=b+a
"
This could be HTML-presented as a
"
Fill in values for
textbox a= _____
textbox b= _____
We have that <value of a>+<value of b>=<value of b>+<value of a>
"https://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.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/5Metalogical formalization of Dynamic Logics2017-07-31T19:36:30ZMichael Kohlhasemichael.kohlhase@fau.deMetalogical formalization of Dynamic LogicsDynamic logics are popular as target systems for semantics construction. There is quite a ariety of them:
* DRT (Kamp & Reyle) and variants (including sDRT and lamba-DRT)
* DPL (Gronendijk and Stokof) and variants (includeing DMG)
* ....Dynamic logics are popular as target systems for semantics construction. There is quite a ariety of them:
* DRT (Kamp & Reyle) and variants (including sDRT and lamba-DRT)
* DPL (Gronendijk and Stokof) and variants (includeing DMG)
* ...
it would be nice if the [LATIN](https://mathhub.info/MMT/LATIN) logic atlas had some of these logics.
The main problem is that we cannot just use the LF metalogical framework directly, but have to extend it with dynammic primitieves. This makes things a lot harder. @dmueller has already worked a bit on this, so he can supervise.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/4A Mathematical Infrastructure for slightly advanced Analysis2017-07-31T19:36:30ZMichael Kohlhasemichael.kohlhase@fau.deA Mathematical Infrastructure for slightly advanced AnalysisWe need for (e.g. #3) an seed infrastructure of flexiformal theories for (a bit more advanced) analysis. On the one hand this could be done in MMT and on the other hand in [the SMGloM](http://smglom.mathhub.info) (actually both, they ...We need for (e.g. #3) an seed infrastructure of flexiformal theories for (a bit more advanced) analysis. On the one hand this could be done in MMT and on the other hand in [the SMGloM](http://smglom.mathhub.info) (actually both, they need also be synchronized by symbols). In particular
* Integrals (Riemann, Lebesque, path, volume, ...)
* Manifolds
* vector fields and tensors
* div/grad representations vs. coordinate representations (can we write down the views?)
* ODEs and PDEshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/3FrameIT for mathematical models.2020-04-27T14:44:15ZMichael Kohlhasemichael.kohlhase@fau.deFrameIT for mathematical models.Mathematical models (e.g. differential equations, ...) are used in many branches of social and natural sciences. There is talk (e.g. by [Karsten Tabelow](http://www.wias-berlin.de/people/tabelow)) of [building collections of math models...Mathematical models (e.g. differential equations, ...) are used in many branches of social and natural sciences. There is talk (e.g. by [Karsten Tabelow](http://www.wias-berlin.de/people/tabelow)) of [building collections of math models as a resource](
http://www.wias-berlin.de/publications/wias-publ/run.jsp?template=abstract&type=Preprint&year=2016&number=2267). I believe that the [FrameIT method](https://www.cicm-conference.org/2016/ceur-ws/W50.pdf) (see also #1) developed at KWARC is exactly the right framework for reprsesenting and applying such models, only that we do not need the game part. The main difference is that we want to explore the real world, not the game world; a main contribution of this thesis might be to design that kind of interaction interface that allows this. Maybe even a "search engine" that suggests math models given a "situation theory".
This application needs to be developed further, and may become a project proposal if successful.
cc: @dmuellerMichael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://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.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/1FrameIT Game Content (Developing a Serious Game for Maths): B.Sc. or M.Sc thesis2022-10-14T15:55:54ZMichael Kohlhasemichael.kohlhase@fau.deFrameIT Game Content (Developing a Serious Game for Maths): B.Sc. or M.Sc thesisWe have developed a new, logic based framework for serious games (see [this paper](https://www.cicm-conference.org/2016/ceur-ws/W50.pdf)), which combines a logic-based treatment of the underlying knowledge in theory graphs with game el...We have developed a new, logic based framework for serious games (see [this paper](https://www.cicm-conference.org/2016/ceur-ws/W50.pdf)), which combines a logic-based treatment of the underlying knowledge in theory graphs with game elements in unreal engine. The aim is to develop serious games (games where the subjects learn somthing while they are having fun) for mathematics.
The current state is that we have developed a proof-of-concept system that can run exactly one game problem. While this is quite an achievement, we need much more for a "serious game". Some of this should be developed in this thesis (actually, this probably needs multiple thesis): Extensions include
* more problem formalizations in MMT ("shadow scaling method", more trig, triangulation, ... )
* more gadgets (3d models) in unreal engine, e.g. laser pointer for marking points, tape measure for lengths, laser angle finder, level pointer, ... )
* more problem situations (game plans), e.g. tree height on non-horizontal ground.
* automatic scroll generation from sTeX/iMMT formalizations
* integration of Semantic Alliance Technology
* didactically informed storyboards for a simple game (where do problems/scrolls come from, levels, boss-fights at the end, ...)
* argumentation interface for "proving" preconditions of methods.
**There has been a big update, see https://uframeit.github.io/!**
Supervisors @mkohlhase, @dmuellerMichael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.de