GitLab

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 (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 or 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).