thesis-projects issueshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues2018-11-24T09:41:32Zhttps://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/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/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 thesis2021-09-02T12:10:49ZMichael 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.dehttps://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/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/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/19MMT as a parser framework for Scala APIs2018-07-02T20:21:23ZFlorian RabeMMT as a parser framework for Scala APIsSee https://github.com/UniFormal/MMT/issues/368See https://github.com/UniFormal/MMT/issues/368https://gl.kwarc.info/kwarc/thesis-projects/-/issues/20Representing Relational Databases in a Logical Framework2019-10-08T11:08:32ZFlorian RabeRepresenting Relational Databases in a Logical Framework@kohlhase @twiesing
There is a very elegant embedding of relational databases into MMT.
* We write a theory D that declares all the basic datatypes (integers, string, products, etc.) of the database language.
* A table schema is repres...@kohlhase @twiesing
There is a very elegant embedding of relational databases into MMT.
* We write a theory D that declares all the basic datatypes (integers, string, products, etc.) of the database language.
* A table schema is represented as a theory S with meta-theory D. The constants of S correspond to the columns of the table.
* Local consistency conditions (which are often omitted in relational databases) are represented as axioms in S.
* A table entry in S is represented as a morphism S -> D, i.e., entries are records whose fields are given by S.
* A join is represented as a pushout.
For example, the join of S with S' where the field f of S should be equal to the field f' of S', is the pushout of {f} -include-> S and {f} -{f=f'}-> S'.
The entries of the join are the set of universal morphisms out of the pushout for every pair (e,e') of entries for which the respective diagram commutes.
* A database view providing a table S backed by a table T are MMT morphisms m is represented as a morphism S -> T.
As a special case, include morphisms represent the selection of some columns from a table.
The entries of the view are the morphisms m;e for all entries e of T.
* A writable view providing S backed by T allows modifying an entry of T if the change can be propagated back to the corresponding entry of T.
If T is a declared theory, this is possible if m is a renaming/inclusion.
If m is a view or join, this is more complicated.
The goal of this topic is to
* work out the details of the above
* investigate the propagation of changes along writable views in general
* determine how these representations can be used to provide added value to database applications
In particular, we could represent the schema of a database in MMT (as sets of theories and views).
The entries would be stored in an actual database.
The theory D can use high-level datatypes, which MMT's codecs translate to the concrete types of the database.
Queries (like joins, selections, and views) can be formulated in MMT and translated to relational queries; conversely, entries can be translated back to MMT views.https://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/22Formalize Haskell Type Classes as a Theory Graph2021-10-21T16:06:03ZFlorian RabeFormalize Haskell Type Classes as a Theory GraphChoose a logical framework, e.g., LF, and formalize (a simple fragment of) Haskell in it.
Then use that theory as a meta-theory for a theory graph containing the standard type classes.
This includes in particular the various kinds of Mo...Choose a logical framework, e.g., LF, and formalize (a simple fragment of) Haskell in it.
Then use that theory as a meta-theory for a theory graph containing the standard type classes.
This includes in particular the various kinds of Monad classes and their implementations
There are multiple variants of Monad, some related by include, some by view.
Interestingly, because Haskell is a programming language, the Monad *laws* are often spelt out in a formal system.
That can lead to confusion, and a clean theory would be very helpful.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/23Formalization of legal content2019-05-02T10:12:22ZMax RappFormalization of legal contentAs part of the ALMANAC-project, we are currently developing new MMT-modules to deal with conflict-laden content. These include context graphs (theory graphs with attack relations), formalizations of nonmonotonic logics and argumentation ...As part of the ALMANAC-project, we are currently developing new MMT-modules to deal with conflict-laden content. These include context graphs (theory graphs with attack relations), formalizations of nonmonotonic logics and argumentation theories (as context graphs or in classical MMT) and computation and visualization components (Embedding of argumentation semantic solvers, TGView graph viewer).
The goal of this project is a first application of these developments in an effort to formalize paradigmatic documents (rulings, example cases) in law. Legal content involves a plethora of interesting formalization challenges such as defeasible reasoning, ambibuity, precedence and argumentation. There for it provides an ideal arena to gain a sense of the current capabilities of our systems as well as the open requirements.
The project would entail choosing a suitable document (or collection of documents) and flexiformalizing it. The final document will include content of various formalization levels which can be visualized and processed by ALMANAC's graphical and computational tools. The undertaking would be closely supervised jointly by members of the ALMANAC-project and our Legal-Tech cooperation partner [Prof. Dr. Axel Adrian](https://www.str2.rw.fau.de/lehrstuhl/honorarprofessor/).https://gl.kwarc.info/kwarc/thesis-projects/-/issues/24Identifying Mathematical Objects up to Canonical Isomorphpism2019-06-04T22:57:39ZFlorian RabeIdentifying Mathematical Objects up to Canonical Isomorphpism@mkohlhase @dmueller
# Motivation
Mathematics pervasively identifies objects if they are canonically isomorphic.
Examples:
* define the rationals as fractions (pairs of integers, quotiented by cancelling), then identify the integer z...@mkohlhase @dmueller
# Motivation
Mathematics pervasively identifies objects if they are canonically isomorphic.
Examples:
* define the rationals as fractions (pairs of integers, quotiented by cancelling), then identify the integer z with the fraction z/1
* the entire number hierarchy N <: Z <: Q etc. is built like above
* elements of ring R are identified with constant polynomials over R
* elements of ring R are identified with elements in localizations over R
* polynomials are identified with the respective elements in the field of fractions
* generators of a group are identified with elements of the generated group (which are technically equivalence classes)
It is very common that
* the isomorphism is from a smaller to a subset of a bigger structure
* the bigger structure is built from the smaller one (i.e., we cannot simply *define* the smaller one as a subset of the bigger one because we need it to build the bigger one)
* the embedding of the smaller into the bigger structure preserves some operations (e.g., the embedding N -> Z is a semiring morphism, the embedding of R into R[X] is a ring moprhism) and can therefore not simply be represented as just a function
* the set preserved properties is extended later on as additional properties are considered (e.g., the embedding N -> Z is also an order morphism)
Virtually all tools for formalized mathematics cannot handle this at all, let alone elegantly.
It requires fundamentally different formal systems that we have not designed yet.
# Idea
For a certain special case, theory morphisms may be a solution:
* We can define the structures as theories and the embedding as a theory morphism, e.g.,
* N={n: type, z: n, s: n->n}
* Z={i: type, z:i, s:i->i, p:i->i, s(p(x)=x, p(s(x)=x, leq:i->i->prop}
* emb: N->Z = {n={x:i|z leq x}, z=z, s=s}
In particular, the theory morphism would capture which operations are preserved.
In this topic, you build a case study formalizing canonical isomorphisms in this way.
You will identify and possibly solve any theoretical or practical problems that come up along the way.
# Technical Problems
## Weak Embeddings
Often the embedding function is not a theory morphism because it does not preserve all properties of a structure s.
Such embeddings can only be expressed as theory morphism out of S if S is an inadequately weak formalization of s.
Often the theory S amounts to specifying a category in which s is the initial object.
More generally, we can think of s as the structure that is freely generated by the syntax of S.
An important special case are non-injective embeddings.
For example, the embedding of the natural numbers into the theory of rings is not necessarily injective.
This can only be expressed as a theory morphism if the natural numbers are formulated without the injectivity of successor.
Similarly, we may have to allow for non-surjective embeddings if we cannot capture the image of the embedding as a predicate subtype (e.g., when embedding natural numbers into real numbers, where the logic cannot express the needed predicate).
In the case of natural numbers, this means the induction axiom should be optional as well.
## Models as Theories
There are multiple ways to represent mathematical structures (here called models) in a formal system.
*Concrete* models of theory T are given as tuples of their universes and operations, e.g., (N,0,1+,*) for the semiring of natural numbers.
(Technically, this tuple also includes proofs of all axioms.)
Concrete models can be represented in two different way:
* internal models: models are represented as record values of a record type corresponding to T
* external models: models are represented as theory morphisms out of T
*Abstract* models of theory T are represented as theories.
These theories contain undefined constants and axioms. Examples are the models for N and Z above.
Typically, these theories M extend T or admit very simpl morphisms, usually injective renamings, T -> M.
The critical idea of this case study is to use abstract models.
This is the only way that allow using theory morphisms for the embeddings.
It remains open how this relates to other, concrete, representations of models.https://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/26More MathWebSearch Instances2020-03-20T07:45:59ZMichael Kohlhasemichael.kohlhase@fau.deMore MathWebSearch InstancesThere are numerous mathematical resources that need [formula search engines](https://search.mathweb.org). Given Christoph Alt's thesis and MWS front-end this is mostly a matter of writing a good harvester. Some examples that come to mind...There are numerous mathematical resources that need [formula search engines](https://search.mathweb.org). Given Christoph Alt's thesis and MWS front-end this is mostly a matter of writing a good harvester. Some examples that come to mind
* The [Stacks Project](https://stacks.math.columbia.edu/) 7000 pages of algebra in LaTeX; see https://github.com/MathWebSearch/frontend/issues/18
* the [OEIS](https://oeis.org), We had a search engine for the formulae at one point, we just need to resurrect and modernize it (see #27)
* ...
And the best would be to create a joint index where MWS searches all of these together. https://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/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/29FrameNet to OMDoc/MMT exporter.2020-04-04T13:40:03ZMichael 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.Max RappMax Rapphttps://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/31Lexicon Management in GLIF2020-04-20T14:32:19ZFrederik SchaeferLexicon Management in GLIF[**GLIF**](https://github.com/kwarc/GLIF) is a framework for describing the translation of natural language into logical expressions.
This requires the specification of a grammar, a target logic, a domain theory in that logic, and a sema...[**GLIF**](https://github.com/kwarc/GLIF) is a framework for describing the translation of natural language into logical expressions.
This requires the specification of a grammar, a target logic, a domain theory in that logic, and a semantics construction (mapping of parse trees into the domain theory).
If you participated in the LBS lecture, you should be familiar with the setup.
Adding a new word (like "woman") to a GLIF pipeline requires the following additions:
* abstract syntax: `woman_N : N;`
* concrete syntax: `woman_N = mkN "woman" "women";` (if e.g. German is also supported: `woman_N = mkN "Frau" feminine;`)
* domain theory: `woman : i -> o`
* semantics construction: `woman_N = woman`
There clearly is a lot of repetition here.
Your task would be to improve this by designing a lexicon format from which the necessary files can be generated automatically.
A naive attempt to write a lexicon entry could look like this:
```
woman
noun
eng: "woman" "women"
ger: "Frau" feminine
```
We probably want customization in different places. For example, the semantics construction for the name John might be `john_PN = john` or `john_PN = [P] P john` depending on the context. Also, not every project uses the resource grammar library, so the operations used in the concrete syntax might vary.
The lexicon management should also be supported in GLIF's Jupyter front-end.
It would also be interesting to take existing lexica and generate a generic lexicon from that, which can be imported into any projects (with the required customization to make it fit in).https://gl.kwarc.info/kwarc/thesis-projects/-/issues/32FrameIT Scroll Rendering2020-12-03T17:44:34ZRichard MarcusFrameIT Scroll RenderingIn the FrameIT project, 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.
We visualize problems or puzzles in the form o...In the FrameIT project, 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.
We visualize problems or puzzles in the form of interactive *scrolls*, where players can input their gathered knowledge to obtain more information and, eventually, solve the problem.
While currently the scroll is visualized as a combination of problem description and a list of input fields, we would prefer a more organic layout and typesetting where you can fill in the blankets directly in the description text.
The biggest technical issue is the rendering of HTML5 and MathML content outside of web browsers, while at the same time allowing interactions between individual elements of the scroll and their counterparts in the game.
Searching for solutions and possibly comparing different ones will be part of this topic.
For more information, please take a look at the [project issue](https://github.com/UFrameIT/UFrameIT/issues/18) and #1.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/33FrameIT Virtual Reality Port2020-04-27T15:56:41ZRichard MarcusFrameIT Virtual Reality PortIn 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.
Our current frameworks aims at supportin...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.
Our current frameworks aims at supporting the development of serious games.
These profit from virtual reality by having intuitive forms of interaction and a more immersive learning experience.
For interaction, we use different *gadgets* and user interfaces, which need to be adapted for use in VR.
Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/34Machine Learning Applications for FrameIT2021-01-29T13:37:41ZRichard MarcusMachine Learning Applications for FrameITIn 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.
Building on the [Unity machine learning ...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.
Building on the [Unity machine learning integration](https://unity3d.com/machine-learning), we would like to teach an agent to play the games developed with the FrameIT method.
Possible approaches may be:
- reinforcement learning via reward function
- imitation learning
- modularizing tasks based on the MMT knowledge formalizationMichael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/35FrameIT State Interface2020-12-03T17:45:48ZRichard MarcusFrameIT State InterfaceIn 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.
Since (formalized) knowledge is generate...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.
Since (formalized) knowledge is generated interactively during runtime, it is difficult to debug with existing MMT utilities.
Accordingly, we need adaptions to make use of these and new concepts to interact with the generated content on the programming language level.
Based on this, we would like to have an interface that helps developers to monitor the state of the underlying knowledge during gameplay.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://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/37FrameIT Multiplayer2020-12-03T17:54:47ZRichard MarcusFrameIT MultiplayerIn 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.
Many game problems or puzzles could also...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.
Many game problems or puzzles could also be solved through cooperation of multiple players.
To implement this in FrameIT, two aspects need to be investigated and tested:
* The general implementation, which could be a multiplayer server or even local multiplayer.
* The FrameIT-specific implementation. We visualize in the form of interactive *scrolls*, where players can input their gathered knowledge to obtain more information and, eventually, solve the problem.
We require concepts how to manage the knowledge input from multiple players. Some scrolls may need to be available globally while others would benefit from each player having his own.
Additional multiplayer interactions are possible: For example, gathered knowledge or scrolls could be traded between players or players could get points and get a ranking in a scoreboard.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/38Integrate Theorem provers into MMT2020-07-30T11:53:04ZMichael Kohlhasemichael.kohlhase@fau.deIntegrate Theorem provers into MMTOMDoc/MMT allows to represent a wide range of logics and reasoning calculi as (meta)-theories via the Curry/Howard isomoprphism. The MMT system supplies automated type- and this proof-checking for all of these out of the box. But it does...OMDoc/MMT allows to represent a wide range of logics and reasoning calculi as (meta)-theories via the Curry/Howard isomoprphism. The MMT system supplies automated type- and this proof-checking for all of these out of the box. But it does not offer any proof automation.
For some logics - e.g. first-order logic - we have very good proof automation - e.g. EProver, Spass, Vampire, the Hammers, ...
So we could get proof automation in MMT by just translating to the input language of these and when they can find a proof obtain back a proof certificicate (translating that into the existing ND calculus we can leave to a later stage).
1. This idea should be implemented in MMT for one instance (e.g. FOLEQ and EProver) so that we can increase proof efficiency (and proofs are the most important check of adequacy of formalizations).
2. Building on this, we want to develop a general infrastructure for more logics and provers
3. Finally, we should extend this to even more logics by using views induced by conservative extensions. These translate "super-logics" back down to the "source logics". If there is a prover for the "source logic", then we can use it in the "super-logic".
This would one of the most important extensions of the OMDoc/MMT ecosystem.
@dmueller @frabeMichael 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/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/42Immersive Knowledge Interaction2020-12-17T14:39:19ZRichard 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/43FrameIT in the Real World2021-01-29T13:30:22ZRichard MarcusFrameIT in the Real WorldIn 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.
For even ...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.
For even better application to real world problems, we want to add support for augmented reality versions with Mobile AR or devices like the hololens.
Therefore, one of the main tasks will be to capture the geometry of the environment and make it possible to place points and measure information based on this.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/44FrameIT on Android2021-04-16T11:53:17ZRichard MarcusFrameIT on AndroidIn 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.
To deploy...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.
To deploy FrameIT games in schools, it is very important to also support Android.
Accordingly, this topic involves adapting current games and features and design new interactions and possibly new games/levels that have synergies with touchscreens.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/45Meta-Data in MathHub2021-03-31T12:55:24ZFlorian RabeMeta-Data in MathHub@mkohlhase @twiesing
MathHub is a huge library of mathematical libraries.
The underlying content format OMDoc supports metadata, which are currently not used in MathHub for display, cross-referencing, etc.
The infrastructure currently...@mkohlhase @twiesing
MathHub is a huge library of mathematical libraries.
The underlying content format OMDoc supports metadata, which are currently not used in MathHub for display, cross-referencing, etc.
The infrastructure currently also does not generate good cumulative statistics about the data that is valuable for display and other user interactions.
This topic will design how such metadata should be efficiently computed and stored and how it can be used to enhance the user experience.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/46Representing Game Levels in MMT (Project or Bachelor Thesis Topic)2021-09-02T12:10:45ZRichard MarcusRepresenting Game Levels in MMT (Project or Bachelor Thesis Topic)In the FrameIT project, 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.
We visualize problems or puzzles in the form o...In the FrameIT project, 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.
We visualize problems or puzzles in the form of interactive *scrolls*, where players can input their gathered knowledge to obtain more information and, eventually, solve the problem.
We want to have the conditions to solve the game level within MMT!
[WIP, description needs update]
das Konzept von Levels in MMT irgendwie repräsentieren (ähnlich wie wir Scrolls in MMT auch in einer strukturierten Art und Weise repräsentieren)
in Metainformationen sowas repräsentieren wie "the level is solved iff dist(C, A) evaluates to a numeric value"
Insb. könnte mensch sich überlegen, dass es durchaus Levelziele geben wird, die nur Unity überprüfen kann, die MMT-extern sein müssen.
Die könnte mensch trotzdem in MMT repräsentieren a la "level is solved iff [some condition mmt can check internally] and [some condition Unity needs to check]"
Geht in Richtung "flexiformale Repräsentation von Levelzielen in MMT"
For more information, please take a look at the [project issue](https://github.com/UFrameIT/UFrameIT/issues/18) and #1.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/47Defining Programming Languages in a Formal Framework2021-10-21T16:06:20ZFlorian RabeDefining Programming Languages in a Formal FrameworkLogical frameworks allow formally defining the syntax and semantics of languages such as type theories and logics.
Here the framework provides the language-independent concepts (names, declarations, typed expressions, proofs, etc.), and ...Logical frameworks allow formally defining the syntax and semantics of languages such as type theories and logics.
Here the framework provides the language-independent concepts (names, declarations, typed expressions, proofs, etc.), and individual languages are defined by specifying the rules to parse and type-check the language-specific concepts (e.g., quantification or function types).
In this project, we extend that approach to also representing programing languages.
We add an *execution* algorithm to the existing algorithms for parsing and type-checking that interprets a program.
Execution creates a heap and stack and then interprets a program step-wise using language-specific rules that describe the effect that the execution of one program step has on stack, heap, and IO.
As concrete case studies and applications, we rigorously define simple programming languages akin to mainstream languages like Java or Haskell.https://gl.kwarc.info/kwarc/thesis-projects/-/issues/48Knowledge-based simulations of virtual worlds in MMT2021-11-12T10:46:29ZFrederik SchaeferKnowledge-based simulations of virtual worlds in MMTIn the LoViWo for logical virtual worlds, we model the possible component types (cog wheels, pistons, ...) of a virtual world as MMT theories.
The interaction between any two component types is also modeled as an MMT theory using axioms ...In the LoViWo for logical virtual worlds, we model the possible component types (cog wheels, pistons, ...) of a virtual world as MMT theories.
The interaction between any two component types is also modeled as an MMT theory using axioms for the physical laws.
A virtual world is a set of instances of these components and their interactions and is modeled as an MMT theory with corresponding imports/structures.
In this project/thesis you build a solver in MMT that can be used by a game engine like unity to compute updates in the virtual world using the knowledge in the MMT description of the world.
Concretely an event in the virtual world creates an update to some of the constants in the MMT theories representing the world.
Using the new values of the constants, MMT must use the axioms to solve for the values of the other constants and send the new values to the game engine. Your focus will be the MMT side using an interface for receiving/sending updates.
In particular we expect that in most cases the axioms will simplify to systems of linear equations, which can be solved easily.
This is presumably true even if the original axioms are non-linear or not even purely equational because we can plug in concrete values for the updated constants and for constants that are marked as non-changing (positions of the cog wheels as opposed to their angles).