Knowledge-based simulations of virtual worlds in MMT
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).