more

paper.tex

@@ -175,6 +175,25 @@ already understood. This practice gives our method the name \frameit as we are c
 theory morphism from the framing theory which represents our knowledge into the framed
 theory which represents our problem.
 
+\begin{wrapfigure}{r}{3cm}\vspace*{-2em}
+	\begin{tikzpicture}[yscale=.7]
+		% Nodes
+		\node[] (p) {$P$};
+		\node[below left = 1cm of p] (a) {$A$};
+		\node[below right = 1cm of p] (b) {$B$};
+		\node[below right = 1cm of a] (c) {$C$};
+
+		\begin{pgfonlayer}{background}
+			\draw[->] (a) -- (p) node [midway,fill=white] {$i_1$};			
+			\draw[->] (b) -- (p) node [midway,fill=white] {$i_2$};
+			\draw[->] (c) -- (a) node [midway,fill=white] {$f$};
+			\draw[->] (c) -- (b) node [midway,fill=white] {$g$};
+			\node[below = 0.25cm of p] (pushout-node) {};
+			\npushout[0]{pushout-node}{pushout-node};
+		\end{pgfonlayer}
+	\end{tikzpicture}\vspace*{-1em}
+\caption{Pushout}\label{fig:pushout}\vspace*{-1em}
+\end {wrapfigure}
 As theories and theory morphisms form a category, MMT is able to derive a pushout from two
 theories $A$ and $B$ if such a pushout exists. A pushout takes two theory morphisms
 $f : C \to A$ and $g : C \to B$ and produces a theory $P$ and two morphisms
@@ -182,8 +201,6 @@ $i_1 : A \to P$ and $i_2 : B \to P$ such that the square commutes. Intuitively,
 pushout $P$ is formed as the union of $A$ and $B$ so that they share exactly
 $C$. \cite{Rabe:tes15} This concept is visualized in Figure \ref{fig:pushout}.
 
-\input{thesis-pushout}
-	
 In the current version of MMT the result of a pushout is a new MMT theory that contains a
 set of simplified declarations. Lastly, MMT provides us with several ways of developing
 services and applications on top of it, we can either use the provided RESTful interface,
@@ -442,8 +459,99 @@ like to generate them from the predefined problem/solution pairs (Generate[0]).
 the generation of scrolls was not part of this research project, nevertheless I identified
 the necessary components of a scroll.
 
-\input{thesis-scrolls.tex}
-
+\begin {wrapfigure}[]{r}{0.58\textwidth}\vspace*{-2em}
+\begin{framed}
+	\resizebox {\columnwidth} {!}
+	{
+		\begin{tikzpicture}[yscale=.7]
+		% nodes	
+		\node[draw, rectangle, style=thy] (mmt-solution-node) at (0, 0)
+		{
+		\begin{tikzpicture}[sharp corners]
+		% Title
+		\node[minimum height = 0.5cm] (mmt-solution-node-title) at (1,0) {Solution Theory};
+		% Content
+		\node[](result) at (1,-0.75) {$|\overline{bc}| = |\overline{ab}| \cdot \tan(\angle_{CAB})$};
+		\end{tikzpicture}			
+		};
+		\node[draw, rectangle, style=thy] (mmt-problem-theory-node) at (0, -4.0)
+		{
+		\begin{tikzpicture}[sharp corners]
+			% Title
+			\node[minimum height = 0.5cm] (mmt-problem-theory-node-title) at (0,0) {Problem Theory};
+			% Content
+			\node[text width=2.4cm] at (0,-1.25) (mmt-problem-theory-node-content)
+			{
+				$a$,$b$,$c$ : point\\
+				$|\overline{ab}|$ : $\mathbb{R}$\\
+				$\angle_{cab}$ : $\mathbb{R}$ \\
+				$p$ : $\vdash \overline{ab} \perp \overline{bc}$
+			};
+		\end{tikzpicture}
+		};
+		\node[draw, rectangle, style=thy] (mmt-solution-vis-node) at (6, 0)
+		{
+			\begin{tikzpicture}[sharp corners]
+			% Title
+			\node[minimum height = 0.5cm] (mmt-solution-node-title) at (1,0) {Solution Theory Visualization};
+			% Content
+			\node[] at (1,-1) (mmt-solution-node-content)
+			{
+				\begin{tikzpicture}[sharp corners]
+				\coordinate (a) at (0,0);
+				\coordinate (b) at (2,0);
+				\coordinate (c) at (2,1);
+				\draw (c)--(b)--(a)--cycle;			
+				\tkzDrawPoints(a,b,c);
+				\tkzLabelPoints[left](a);
+				\tkzLabelPoints[right](b,c);
+				\tkzLabelSegment[below=2pt](a,b){};
+				\tkzLabelSegment[left=2pt](a,c){};
+				\tkzMarkAngle[fill= green,size=0.75cm, opacity=0.4](b,a,c);
+				\tkzLabelAngle[pos=0.55](b,a,c){$\alpha$};
+				\tkzMarkRightAngle[fill=green,size=0.2, opacity=0.4](a,b,c);
+				\tkzLabelAngle[](a,b,c){};
+				\end{tikzpicture}
+			};
+		\end{tikzpicture}			
+		};
+		\node[draw, rectangle, style=thy] (mmt-problem-theory-vis-node) at (6, -4.0)
+		{
+		\begin{tikzpicture}[sharp corners]
+		% Title
+		\node[minimum height = 0.5cm] (mmt-problem-theory-node-title) at (1,0) {Problem Theory Visualization};
+		% Content
+		\node[] at (1,-1) (mmt-problem-theory-node-content)
+		{
+			\begin{tikzpicture}[sharp corners]
+			\coordinate (a) at (0,0);
+			\coordinate (b) at (2,0);
+			\coordinate (c) at (2,1);
+			\tkzDrawPoints(a,b,c);
+			\tkzLabelPoints[left](a);
+			\tkzLabelPoints[right](b,c);			
+			\draw (c)--(b)--(a);
+			%\draw[<->, thin] (tp2.south east) -- (tp1.north east)
+			%node[midway, right] {$h$};
+			\tkzMarkRightAngle[fill=green,size=0.4, opacity=0.4](a,b,c)
+			\tkzLabelAngle[](a,b,c){};
+			\end{tikzpicture}
+		};
+		\end{tikzpicture}
+		};
+
+		\begin{pgfonlayer}{background}
+		% Scroll Edge
+		\draw[->, black, thick, style=include] (mmt-problem-theory-node) -- (mmt-solution-node);
+		\draw[->, black, thick, style=include] (mmt-problem-theory-vis-node) -- (mmt-solution-vis-node);
+		\draw[->, black, thick, style=include] (mmt-problem-theory-vis-node) -- (mmt-problem-theory-node);
+		\draw[->, black, thick, style=include] (mmt-solution-vis-node) -- (mmt-solution-node);
+		\end{pgfonlayer}
+	\end{tikzpicture}		
+}
+\end{framed}
+\caption{Problem Solution Pair Extension}\label{fig:FrameITProblemSolPairExt}\vspace*{-1em}
+\end {wrapfigure}
 While the current form of problem/solution pairs works perfectly for our present
 implementation, for future implementations and for the generation of scrolls they need to
 be extended and refined. The goal behind this extension would be to include visualization
@@ -462,6 +570,7 @@ output. The OMDoc format\cite{Kohlhase:OMDoc1.2} might be the ideal format here
 allows us to store formal and informal information.
 
 \subsection{\frameit as a Method for Learning}\label{sec:method:learning}
+
 The \frameit method facilitates learning by prompting the user to solve real world
 problems, which he or she can only solve by using scrolls. In the process of solving these
 problems the user starts to understand the theories and approaches presented in each
@@ -478,8 +587,25 @@ of several problems as the user has to find out the height $h$, the height from
 up to his or her eyes and to reason that the absolute tree height is the sum of both.
 
 \section{Design and Implementation}\label{sec:DesignAndImplementation}
-\input{thesis-system-arch} 
-
+\begin {wrapfigure}[]{r}{0.382\textwidth}\vspace*{-2em}
+\begin{framed}
+	\resizebox {\columnwidth} {!}
+	{
+	\begin{tikzpicture}[baseline=(user-node),yscale=.8]
+		% Nodes
+		\node[draw, rectangle] (user-node) at (0,0) {User};
+		\node[draw, rectangle] (ue4-node) at (0,-2) {Game (Unreal Engine)};
+		\node[draw, rectangle] (mmt-node) at (0,-4.5) {MMT};
+
+		\draw[<->, black, thick] (user-node) -- (ue4-node) node [midway,fill=white] {\small interact};
+		\draw[->, black, thick,out=270, in=180,bend angle=70,looseness=1.3] ($(ue4-node.south)+(-1, 0)$) to node[pos = 0.375, fill=white](mid-edge-node-gen3){\small generate theories} ($(mmt-node.west)-(0,0.0)$);
+		\draw[<-, black, thick,out=270, in=360,bend angle=70,looseness=1.3] ($(ue4-node.south)+(1, 0)$) to node[pos = 0.375, fill=white](mid-edge-node-gen3){\small pushout} ($(mmt-node.east)-(0,0.0)$);
+	\end{tikzpicture}		
+	}
+\end{framed}
+\caption{System Architecture}
+\label{fig:systemArch}
+\end {wrapfigure}
 Building up on the refined \frameit method, I designed and implemented a proof of concept
 serious math game that demonstrates our method. Moreover, this first implementation allows
 us to critically assess the method and to discover any shortcomings.

thesis-pushout.tex

-\begin {wrapfigure}{r}{0.382\textwidth}
-\centering
+\begin{wrapfigure}{r}{3cm}\vspace*{-2em}
 	\begin{tikzpicture}[]
 		% Nodes
 		\node[] (p) {$P$};
@@ -15,8 +14,6 @@
 			\node[below = 0.25cm of p] (pushout-node) {};
 			\npushout[0]{pushout-node}{pushout-node};
 		\end{pgfonlayer}
-	\end{tikzpicture}		
-
-\caption{Pushout}
-\label{fig:pushout}
+	\end{tikzpicture}\vspace*{-1em}
+\caption{Pushout}\label{fig:pushout}\vspace*{-1em}
 \end {wrapfigure}