thesis-projects issueshttps://gl.kwarc.info/kwarc/thesis-projects/-/issues2022-03-28T15:20:44Zhttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/50Formal verifcation of evolving software2022-03-28T15:20:44ZFlorian RabeFormal verifcation of evolving softwareVerified software usually consists of
* a formal specification
* an implementation (in the same or a different language than the specification)
* a proof that the latter conforms to the former
When the specification changes, the typical...Verified software usually consists of
* a formal specification
* an implementation (in the same or a different language than the specification)
* a proof that the latter conforms to the former
When the specification changes, the typical practice is to publish new revisions of all three and move the old versions to history.
However, if the old version of the software has been heavily used, it may not be possible to simply replace it.
For example, if the old version was used to process input, it is not guaranteed at all that the new version will interpret the legacy input in exactly the same way as the old one did (even if the new implementation conforms to the new specification).
Instead, it is necessary to additionally relate the semantics of old and new version.
Very little theoretical work and/or practical tools for this change management problem exist.
In this project, you will solve this problem for a simple language (as complicated as we can manage) and develop a method for establishing formal theorems that relate old and new version.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).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/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/42Immersive Knowledge Interaction2021-12-17T13:13:01ZRichard MarcusImmersive Knowledge InteractionIn the FrameIT project (#1 and https://uframeit.github.io), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Currently...In the FrameIT project (#1 and https://uframeit.github.io), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Currently, the player can only interact with knowledge items via a special UI that mirrors the knowledge formalized in MMT as *scroll*. This 2D UI causes a cognitive dissonance to the 3D world that it talks about. A more immersive solution would fit better (at least for some applications)
For more immersion, we would like to
- a) automatically synchronize certain facts about the world dynamically (e.g. for moving objects)
- b) use in-game triggers to communicate with the logic engine
- c) have in-game interfaces to communicate with the logic engine
- d) allow players to directly assign objects somehow instead of using the corresponding generated icons
or build other features that result in more fluent gameplay.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/41Linking Formalized Situations to specific Game Objects/Situations2020-12-20T09:26:44ZRichard MarcusLinking Formalized Situations to specific Game Objects/SituationsIn the FrameIT project (#1), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Based on parametric situation theories, ...In the FrameIT project (#1), we use the Unity game engine in combination with MMT to have access to mathematical knowledge management techniques and interact with the knowledge in the game world.
Based on parametric situation theories, which are instantiated by "pretty small Unity scripts", we want to link the parameters to specific points in the world modeled in Unity.
Our goal here is to create a toolkit for game developers that allows them to integrate the formalized knowledge into the games in the form of modular elements that can linked to game objects.
Work Areas:
- 1. Making the formalized knowledge available to the Unity Editor itself (https://learn.unity.com/tutorial/editor-scripting#), which could enable interactions like this:
- list available fact types so that developers can select which gadgets can create these facts
- list available scrolls so that developers can build levels based on the problems defined in the scrolls
- 2. Scripting the generation of semantic game objects
- we could define certain object attributes on the knowledge side like "base_tree"
- if the developer assigns this attribute to an object in the game it should then be enhanced automatically: place it in a 90 degree angle to the ground, generate snapzones for root and top, configure colliders
- 3. Advanced Toolkit Interactions based on 1 and 2, e.g., if a Fact is connected to a Gadget, we know which Gadget should be used to create a certain fact for a solution
- 4: Building a graphical tool for this. Unity recently acquired [Bolt](https://assetstore.unity.com/packages/tools/visual-scripting/bolt-163802). Maybe it could be integrated into this, maybe we want/need our own editor, needs investigation.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/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/37FrameIT Multiplayer2023-02-05T00:51:15ZRichard 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/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/34Machine Learning Applications for FrameIT2023-02-03T10:26: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://unity.com/products/machine-learning-agents), 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 formalization
Note that there is no groundwork for this topic, so a strong background in machine learning is required.Michael Kohlhasemichael.kohlhase@fau.deMichael Kohlhasemichael.kohlhase@fau.dehttps://gl.kwarc.info/kwarc/thesis-projects/-/issues/33FrameIT Virtual Reality Port2023-01-20T22:14:44ZRichard 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/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/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/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/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/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/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.de