Reusing Learning Objects via Theory Morphisms

One of the most important motivations of module systems for formal systems is that statements and objects can be re-purposed in other contexts via the inheritance pathways. In this paper, we show that this idea can be extended to informal settings using an adaptive learning assistant (ALeA) as a concrete use case. Specifically, we concentrate on repurposing informal definitions, quiz questions, and explanations between the contexts given by different theories in a flexiformal theory graph. Using this, we can now refactor (transport backwards over a theory morphism) e.g. quiz questions like “Is the following formula \(\textit{A}\) satisfiable?” to be logic-independent and utilize them in any logic via forward morphism transport. This goes a large step towards solving the biggest practical problem in ALeA-like systems: provisioning enough targeted semantically annotated learning objects.