Unverified Commit 4645012d authored by Tom Wiesing's avatar Tom Wiesing
Browse files

Add Tom Wiesing Thesis

parent c78505b5
# Bachelor Thesis Repository
This is the source for the write-ups of my Bachelor Thesis (the actual code is in other places).
There are 3 parts to this:
* ```proposal/``` - The proposal for the topic
* ```thesis/``` - The actual thesis write-up
* ```presentation/``` - The beamer-latex used for my presentation
Assuming you have ``latexmk`` installed, you should be able to compile these by just running `make`.
## License
© Tom Wiesing 2015
![Creative Commons License](https://i.creativecommons.org/l/by-nc-nd/3.0/88x31.png)
This work is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by-nc-nd/3.0/">Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License</a>.
LFLAGS = -pdf
all: graph1 master
clean: cleanmaster cleangraph1
master: setupmaster
cd dest && latexmk $(LFLAGS) presentation.tex
cd dest && cp presentation.pdf ..
mkdir -p dest
cp -r *.tex imgs dest
rm -rf dest
rm -f presentation.pdf
graph1: setupgraph1
cd graph1/dest && pdflatex -shell-escape graph1.tex
cd graph1/dest && convert -density 500 -resize 1920x1080 graph1.pdf graph1.png
cd graph1/dest && cp graph1.png ../../imgs/graph1.png
cd graph1 && mkdir -p dest
cd graph1 && cp *.tex dest
cd graph1 && rm -rf dest
cd imgs && rm -rf graph1.png
% Input encoding
% Math packages
\draw[rounded corners, draw=none, fill=lightgray, opacity=0.5] (-1.7,-3.5) -- (-1.7,-0.5) -- (0.4,-0.5) -- (0.4,-3.5) -- cycle;
% Theory of Dimensions
\node[thy] (dim) at (-1,-3) {
8 basic dimensions\\
dimension multiplication\\
dimension division\\
% Dimensions extended
\node[thy] (dimex) at (-1,-2) {
\textsf{Dimensions Extended}\\\hline
aliases for composite dimensions\\
(such as $\mathsf{area} = \mathsf{length} \cdot{} \mathsf{length}$)\\
\draw[include] (dim) -- (dimex);
\node[thy] (numbers) at (0,-2) {
basic numbers\\
% Quantity Expressions
\node[thy] (qes) at (-0.75,-1) {
\textsf{Quantity Expressions}\\\hline
quantity expression constructors\\
quantity expression multiplication\\
quantity expression division\\
\draw[include] (numbers) -- (qes);
\draw[include] (dimex) -- (qes);
\node[thy] (SI) at (-1,0) {
basic SI units for all dimensions\\
\draw[include] (qes) -- (SI);
%Imperial Lengths 1A
\node[thy] (ImpA1) at (0.3,0) {
\textsf{Imperial Lengths A1}\\\hline
\draw[include] (qes) -- (ImpA1);
\draw[view] (ImpA1) -- (SI);
%Imperial Lengths A2
\node[thy] (ImpA2) at (1.5,0) {
\textsf{Imperial Lengths A2}\\\hline
Inch, Foot, Yard, \\
Chain, Fathom, Mile, \\
Mile, Furlong, Cable, \\
Nautical Mile, League\\
\draw[include] (ImpA1) -- (ImpA2);
%Imperial Lengths B1
\node[thy] (ImpB1) at (0.9,-1) {
\textsf{Imperial Lengths B1}\\\hline
\draw[include] (qes) -- (ImpB1);
\draw[view] (ImpB1) -- (ImpA2);
%Imperial Lengths B2
\node[thy] (ImpB2) at (1,-2) {
\textsf{Imperial Lengths B2}\\\hline
\draw[include] (ImpB1) -- (ImpB2);
% Imperial Lengths
\node[thy] (ImpLen) at (1.75,-1) {
\textsf{Imperial Lengths}\\\hline
\draw[include] (ImpA2) -- (ImpLen);
\draw[include] (ImpB2) -- (ImpLen);
% Imperial Area
\node[thy] (ImpArea) at (1.75,-2.7) {
\textsf{Imperial Area}\\\hline
Perch, Rood, Acre\\\hline
\draw[include] (ImpLen) -- (ImpArea);
% A TIKZ library for MMT Theory Graphs
% copyright 2014 Michael Kohlhase; Released under the LPPL
% this library provides some standardized node and arrow styles for formatting MMT graph
% diagrams in tikz. The advantage is that we can classify the arrows and nodes
% symbolically and with the styles in this library achieve a uniform look that helps
% readability.
%%% 1. Theories
% a generic theory
\tikzstyle{thy}=[draw,outer sep=\outerthysep,rounded corners,inner sep=\innerthysep]
% a primitive theory
% a theory graph
\tikzstyle{thygraph}=[draw,outer sep=1mm,rounded corners,dashed]
%%% 2. Arrows
%%% 2.1. Arrowtips (only internal)
\newcommand{\@mmtarrowtip}{angle 45}
\newcommand{\@mmtreversearrowtip}{angle 45 reversed}
\newcommand{\@mmtarrowtipepi}{triangle 45}
\newcommand{\@mmtarrowtipmonoright}{right hook}
\newcommand{\@mmtarrowtipmonoleft}{left hook}
\newcommand{\@mmtarrowtippartial}{right to}
\newcommand{\@mmtarrowtippartialleft}{left to}
\newcommand{\@mmtreversearrowtippartial}{right to reversed}
\newcommand{\@mmtreversearrowtippartialleft}{left to reversed}
%%% 2.2 the arrow sstyles in graphs
% any morphism
\tikzstyle{mapsto}=[|-\@mmtarrowtip] %| any morphism
% structures
% inclusions: regular, partial, and left variants
% views: regular, mono, partial, and left variants
segment length=6pt,
pre=lineto,pre length=3pt,
post=lineto,post length=5pt},
% biviews: regular, partial, and left variants
% defining views (experimental)
\tikzstyle{defview}=[preview,densely dotted,-\@mmtarrowtip]
% meta-theory inclusion
% conservative extensions (abbreviation)
% conservative development
% antimorphisms as striktthroughs
decoration={markings, mark=between positions 0.2 and 0.8 step 4mm with {
\draw [thick,-] ++ (-3pt,-3pt) -- (3pt,3pt);}},
% parallel markup
%%% 3. convenience macros
%%% 3.1 the \mmtthy macro takes three arguments, name, decl, axioms and makes a
% table-like structure
\begin{array}{l}\textsf{#1}\\\hline #2\ifx\@test\@empty\else\\\hline #3\fi\end{array}}
%%% 3.2 the \mmtar takes two arguments, some tikz options, and an arrow style. \nmmtar
% is a variant that also has a name on top.
\newcommand\mmtar[2][]{\raisebox{.5ex}{\tikz[#1]{\draw[#2] (0,0) -- (.6,0);}}}
\newcommand\nmmtar[3][]{\raisebox{.4ex}{\tikz[#1]{\draw[#2] (0,0) --
node[above]{\ensuremath{\scriptstyle #3}} (.8,0);}}}
% Do some customisations
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
\title{Semantic Search for Quantity Expressions}
\author{Tom Wiesing\\\ \\Supervisor: Michael Kohlhase\\Co-supervisor: Tobias Preusser}
\date{May 20, 2015 \\110392 Guided Research Applied and Computational Mathematics \& Thesis}
\begin{frame}{Semantic Search for Quantity Expressions}
\item Motivation: Problem and State Of The Art
\item Our Approach: Structure Of The Search Engine
\item The Unit System
\item The Search Algorithm
\item The Implementation
\item Time for Questions
\begin{frame}{Motivation (1)}
\item We use units every day
\item We encounter them everywhere:
\item When driving, there are speed limits, for example: \raisebox{-0.5\height}{\includegraphics[width=10mm]{imgs/sign60.png}} $\frac{\text{km}}{\text{h}}$
\item When baking, it often says in recepies something like: ``add 3 tea spoons of sugar''
\item When shopping for shoes there are different sizes
\item In scientific papers they occur a lot
\item everything which somehow models a real system has at least one quantity expression
\item everything is quantified
\begin{frame}{Motivation (2)}
\item within one paper, commonly only one type of units is used
\item In general there are \textbf{a lot} of \textbf{different} units to describe \textbf{the same} quantity
\item Just for lengths: \pause \textit{Meter}, \pause \textit{Inch}, \pause \textit{Foot}, \pause \textit{Mile}, \pause \textit{Nautical Mile}, \pause $\dots$
\item This can cause problems when not converting properly
\item Mars Climate Orbiter (1999) \\ \includegraphics[width=50mm]{imgs/mco.jpg}
\begin{frame}{Motivation (3)}
\item Most common solution: Unit Converters
\item There are a lot of these \\ \includegraphics[width=40mm]{imgs/google.png}
\item Google itself has one integrated \\ \includegraphics[width=40mm]{imgs/googleuc.png}
\begin{frame}{Motivation (4)}
\item A lot of user interaction:
\item Problem identification
\item input units \& output units
\item not integrated into search process
\item Wouldn't it be nice:
\item when searching for $90\ \frac{\text{km}}{\text{h}}$
\item we also find $25\ \frac{\text{m}}{\text{s}}$
\item This is the kind of search engine we have built
\begin{frame}{Our Approach (1)}
\item What components do we need for a semantic search engine?
\item A \textit{Unit System} that is aware of the different representations of a QE
\item A \textit{Spotter} that finds representations of QEs inside documents
\item A \textit{Search Algorithm} that given a QE finds all its representations in the system
\item A \textit{Frontend} that allows queries to be made
\item Spotter is done by \textit{Stiv Sherko}
\begin{frame}{Our Approach (2)}
\item Meta-mathematical model: used to describe structure of mathematics
\item \textit{Theory} = List of \textit{Definitions}
\item \textit{Term} = Expression written using definitions from a Theory
\item Theories can be related in 2 ways:
\item \textit{Import}s make Definitions from one theory available in another
\item \textit{View} = truth-preserving mapping between theories
\item Can be displayed in a \textit{Theory Graph}
\item \textit{MMT} = software that implements these concepts
\item easy to write down theories without programming knowledge
%Unit System
\begin{frame}{Our Approach: The Unit System (1)}
\item Need a \textit{Theory of Quantity Expressions} (QEs)
\item Each quantity has a dimension
\item According to SI there are 7 basic ones:
\item length
\item mass
\item time
\item electric current
\item temperature
\item luminous intensity
\item amount of substance
\item but there are also quantities where we just \textit{count}
\item and \textit{dimensionless quantities} (such as Information)
\item so we have 9 basic dimensions
\begin{frame}{Our Approach: The Unit System (2)}
\item we can also multiply these to get new dimensions
\item area $=$ length $\cdot{}$ length
\item similarly we can divide dimensions
\item velocity $= \frac{\text{length}}{\text{time}}$
\begin{frame}{Our Approach: The Unit System (3) - A Theory of Dimensions}
\begin{tabular}{|l l l|}
\textsf{Dimension} & &\\\hline
$\mathsf{dim}$ & $:$ & $ \mathsf{type}$\\
$\mathsf{none}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{count}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{length}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{mass}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{time}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{current}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{temperature}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{luminous}$ & $:$ & $ \mathsf{dim}$\\
$\mathsf{amount}$ & $:$ & $ \mathsf{dim}$\\
$\cdot{}$ & $:$ & $ \mathsf{dim} \rightarrow \mathsf{dim} \rightarrow \mathsf{dim}$\\
$/$ & $:$ & $ \mathsf{dim} \rightarrow \mathsf{dim} \rightarrow \mathsf{dim}$\\\hline
\begin{frame}{Our Approach: The Unit System (4)}
\item Quantity Expressions can be one of
\item \textit{primitive unit}, such as Meter
\item \textit{Multiplication} of a (real) number with an existing QE, such as $5\ \text{Meter}$
\item \textit{Division} of an existing QE by a (non-zero real) number (equivalent to the above)
\item \textit{Product} of two existing QEs such as $\text{Newton} \cdot{} \text{Second}$
\item \textit{Quotient} of two existing QEs such as $1\ \frac{\text{Meter}}{\text{Second}}$
\item \textit{Sum} of two existing QEs
\begin{frame}{Our Approach: The Unit System (5) - A Theory of Quantity Expressions}
\begin{tabular}{|l l l|}
\textsf{Quantity Expression} & &\\\hline
$ \mathsf{import \ Dimension}$ &&\\\hline
$\mathsf{QE}$ & $:$ & $ \mathsf{dim} \rightarrow \mathsf{type}$\\
$\mathsf{QENMul}$& $:$ & $ \forall x : \mathsf{dim} . \realnz \rightarrow \mathsf{QE}\left( x\right) \rightarrow \mathsf{QE}\left( x\right)$\\
$\mathsf{QENDiv}$& $:$ & $ \forall x : \mathsf{dim} . \mathsf{QE}\left( x\right) \rightarrow \realnz \rightarrow \mathsf{QE}\left( x\right)$\\
$\mathsf{QEAdd}$& $:$ & $ \forall x : \mathsf{dim} . \mathsf{QE}\left( x\right) \rightarrow \mathsf{QE}\left( x\right) \rightarrow \mathsf{QE} \left( x \right) $\\
$\mathsf{QEMul}$& $:$ & $ \forall x, y : \mathsf{dim} . \mathsf{QE}\left( x\right) \rightarrow \mathsf{QE}\left( y\right) \rightarrow \mathsf{QE} \left( x \cdot{} y \right) $\\
$ \mathsf{QEDiv}$& $:$ & $ \forall x, y : \mathsf{dim} . \mathsf{QE}\left( x\right) \rightarrow \mathsf{QE}\left( y\right) \rightarrow \mathsf{QE} \left( \frac{x}{y} \right) $\\\hline
\begin{frame}{Our Approach: The Unit System (6)}
\item we can now easily create theories that define Units, such as a Meter Theory:
\begin{tabular}{|l l l|}
\textsf{Meter} &&\\\hline
$ \mathsf{import \ Quantity\ Expression}$ &&\\
$\mathsf{Meter}$ & $:$ & $ \mathsf{QE} \left( \mathsf{length} \right)$\\\hline
\item we can also define some non-metric lengths:
\textsf{Non SI Lengths}\\\hline
$ \mathsf{import \ Quantity\ Expression}$\\
$\mathsf{Thou} : \mathsf{QE}\left( \mathsf{length} \right)$\\
$\mathsf{Foot} = \mathsf{QENMul} \left( 1000, \mathsf{Thou} \right)$\\
$\mathsf{Yard} = \mathsf{QENMul} \left( 3, \mathsf{Foot} \right)$\\
$\mathsf{Chain} = \mathsf{QENMul} \left( 22, \mathsf{Yard} \right)$\\
$\mathsf{Furlong} = \mathsf{QENMul} \left( 10, \mathsf{Chain} \right)$\\
$\mathsf{Mile} = \mathsf{QENMul} \left( 8, \mathsf{Furlong} \right)$\\
\begin{frame}{Our Approach: The Unit System (7)}
\item need to compare units
\item use \textit{Views} ( = truth-preserving mappings between theories)
\item For example: