Commit 307f4d85 authored by Michael Banken's avatar Michael Banken

added blabla

parent 63d52115
......@@ -9,4 +9,14 @@
@misc{MMTapi, title={{MMT API Documentation}}, howpublished = {\url{https://uniformal.github.io/apidoc/index.html}}, journal={MMT Documentation}, publisher={uniformal.github.io}, note={Accessed: 2018-06-20}}
@misc{latin, title={{MMT/LATIN}}, howpublished = {\url{https://gl.mathhub.info/MMT/LATIN}}, journal={mathhub}, publisher={gl.mathhub.info}, note={Accessed: 2018-06-26}}
\ No newline at end of file
@misc{latin, title={{MMT/LATIN}}, howpublished = {\url{https://gl.mathhub.info/MMT/LATIN}}, journal={mathhub}, publisher={gl.mathhub.info}, note={Accessed: 2018-06-26}}
@article{rabe2013scalable,
title={A scalable module system},
author={Rabe, Florian and Kohlhase, Michael},
journal={Information and Computation},
volume={230},
pages={1--54},
year={2013},
publisher={Elsevier}
}
\ No newline at end of file
\chapter{Introduction}
\section{Motivation}
Knowledge is complicated and so is its representation.
Knowledge is complicated and so is its representation, especially when trying to store it in a computer. One approach to solve this issue is by organizing bodies of knowledge in neat graph structures. A project that seeks to model knowledge in this way is the MMT language\cite{rabe2013scalable}, which has theory graphs as its semantics. Unfortunately the graph structures which are generated represent the knowledge so well that they inherent its complexity.
\begin{figure}[!htb]
\centering
......@@ -10,6 +10,8 @@ Knowledge is complicated and so is its representation.
\label{fig:tgview}
\end{figure}
Since these theory graphs can be massive in size, it should not be surprising that like any other large project they can be plagued by redundancies and entirely unnecessary dependencies.
For this reason it should be no surprise that these theory graphs can be plagued by redundancies and entirely unnecessary dependencies.
To help reduce unnecessary complexity of these theory graphs, I introduce Styler, an automated tool for optimizing theory inclusions.
\ No newline at end of file
To help reduce unnecessary complexity of these large theory graphs, I introduce Styler, an automated tool for optimizing theory inclusions.
The goal of this tool is to automatically detect possible optimizations that reduce the number of edges without breaking the graph and recommend them to the user.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment