diff --git a/slides/examples/assignments.lp b/slides/examples/assignments.lp
deleted file mode 100644
index 3564d9b..0000000
--- a/slides/examples/assignments.lp
+++ /dev/null
@@ -1,4 +0,0 @@
- #($\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} = x$#) :- #($\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} := x$#),
-                  def(#($x_1$)#),#(\dots#),def(#($x_n$)#).
-&sum{#($l$#)} <= #($x$#) :- #($\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$#).
-&sum{#($u$#)} >= #($x$#) :- #($\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$#).
diff --git a/slides/examples/conditional.lp b/slides/examples/conditional.lp
deleted file mode 100644
index b5e489b..0000000
--- a/slides/examples/conditional.lp
+++ /dev/null
@@ -1,9 +0,0 @@
-&sum{#($\mathit{aux}_i$#)} = #($\mathit{e}_i$#) :- #($\mathit{c}_i$#), def(#($x_1$)#),#(\dots#),def(#($x_n$)#).
-&sum{#($\mathit{aux}_i$#)} = #($0_t$#) :- not #($\mathit{c}_i$#).
-&sum{#($\mathit{aux}_i$#)} = #($\mathit{e}_i$#) :- #($\mathit{c}_i$#), def(#($\mathit{aux}_i$#)).
-&sum{#($\mathit{aux}_i$#)} = #($0_t$#) :- not #($\mathit{c}_i$#), def(#($\mathit{aux}_i$#)).
-{#($\mathit{c}_i$#)} :- def(#($\mathit{aux}_i$#)).
-#($\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k$#) :-
-            #($\mathtt{\&}t(l)\mathtt{\{}\dots,\mathit{aux}_1,\dots,\mathit{aux}_n,\dots\mathtt{\}} \prec k$#).
-#($\mathtt{\&}t(l)\mathtt{\{}\dots,\mathit{aux}_1,\dots,\mathit{aux}_n,\dots\mathtt{\}} \prec k$#)   :-
-            #($\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k$#).
diff --git a/slides/examples/cp_lang.lp b/slides/examples/cp_lang.lp
deleted file mode 100644
index 6ce76c2..0000000
--- a/slides/examples/cp_lang.lp
+++ /dev/null
@@ -1,16 +0,0 @@
-#theory csp {
-    var_term  { };
-    sum_term {
-        #($\cdots$#)
-    };
-    dom_term {
-        #($\cdots$#)
-    };
-    #(\alert<2->{\&sum/1 : sum\_term, \{<=,=,!=,<,>,>=\}, sum\_term, any;} #)
-    &diff/1 : sum_term, {<=}, sum_term, any;
-    &minimize/0 : sum_term, directive;
-    &maximize/0 : sum_term, directive;
-    &show/0 : sum_term, directive;
-    &distinct/0 : sum_term, head;
-    &dom/0 : dom_term, {=}, var_term, head
-}.
diff --git a/slides/examples/htc_lang.lp b/slides/examples/htc_lang.lp
deleted file mode 100644
index f0aa946..0000000
--- a/slides/examples/htc_lang.lp
+++ /dev/null
@@ -1,19 +0,0 @@
-#theory htc {
-    sum_term {
-    -  : 3, unary;
-    ** : 2, binary, right;
-    *  : 1, binary, left;
-    /  : 1, binary, left;
-    \\ : 1, binary, left;
-    +  : 0, binary, left;
-    -  : 0, binary, left
-    };
-    dom_term {
-        #($\cdots$#)
-    .. : 0, binary, left
-    };
-    &sum/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any;
-    &min/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any;
-    &max/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any;
-    &in/1 : dom_term, {=:}, sum_term, head
-}.
diff --git a/slides/examples/minmax.lp b/slides/examples/minmax.lp
deleted file mode 100644
index dd2b738..0000000
--- a/slides/examples/minmax.lp
+++ /dev/null
@@ -1,7 +0,0 @@
-def(#($\mathit{min}$#)) :- def(#($x_1$)#),#(\dots#),def(#($x_n$)#).
-:- not &sum(body){$\mathit{min}$} <= $e_i$.
-s :- sum(body){$\mathit{min}$} = $e_i$.
-:- not s, def(#($\mathit{min}$#)).
-&min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$ :- &sum$(l)\{\mathit{min}\} \prec k$, def(#($\mathit{min}$#)).
-&min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$ :- &sum$(l)\{\mathit{min}\} \prec k$.
-&sum$(l)\{\mathit{min}\} \prec k$ :- &min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$.
diff --git a/slides/examples/semantics.lp b/slides/examples/semantics.lp
deleted file mode 100644
index 3933467..0000000
--- a/slides/examples/semantics.lp
+++ /dev/null
@@ -1,23 +0,0 @@
-a :- &sum{x} = 1.
-a :- &sum(body){x} = 1.
-&sum(head){ #($e_1,\dots,e_n$#) } #($\prec k$#)
-def(x) :- &sum(head){ #($e_1,\dots,e_n$#) } #($\prec k$#).
-&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)
-&sum(#($l$#)){ #($e_1,\dots,e_n$#) } #($\prec k$#).
-&sum{x} = 0 :- not def(x).
-&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)
-'&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)'
-            :- &sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#),
-               def(x#($_1$#)),#($\dots$#),def(x#($_n$#)).
-{&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)}.
-c :- &sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#),
-     def(x#($_1$#)),#($\dots$#),def(x#($_n$#)).
-{&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)}.
-a :- '&sum{x} = 1'.
-'&sum{x} = 1' :- &sum{x} = 1, def(x).
-{&sum{x} = 1}.
-&sum{x} = 0 :- not def(x).
-a :- c.
-c :- &sum{x} = 1, def(x).
-{&sum{x} = 1}.
-&sum{x} = 0 :- not def(x).
diff --git a/slides/examples/taxes.lp b/slides/examples/taxes.lp
deleted file mode 100644
index 4773142..0000000
--- a/slides/examples/taxes.lp
+++ /dev/null
@@ -1,29 +0,0 @@
-person(paul;mary).
-region(luxemburg;germany).
-rate(germany,  25000, 15).
-rate(germany,  50000, 25).
-rate(germany, 100000, 35).
-rate(luxemburg,  38700, 14).
-rate(luxemburg,  58000, 23).
-rate(luxemburg,  96700, 30).
-income(paul,   60000).
-income(mary,  120000).
-deduction(mary, 10000, 10001).
-
-1 { lives(P,R) : region(R) } 1 :- person(P).
-
-&sum{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_).
-&in{ L..H } =: deduction(P) :- deduction(P,L,H).
-&sum{ T } =: rate(P) :- lives(P,R), income(P,I),
-                        T = #max{ T' : rate(R,L,T'), I>=L}.
-
-&sum{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I).
-&sum{ tax(P) : lives(P,R) } =: total(R) :- region(R).
-&min{ tax(P) : person(P) } =: min.
-&max{ tax(P) : person(P) } =: max.
-min_taxes(P) :- &min{ tax(P') : person(P') } = tax(P), person(P).
-max_taxes(P) :- &max{ tax(P') : person(P') } = tax(P), person(P).
-
-#show lives/2.
-#show min_taxes/1.
-#show max_taxes/1.
diff --git a/slides/examples/vicious.lp b/slides/examples/vicious.lp
deleted file mode 100644
index 1586429..0000000
--- a/slides/examples/vicious.lp
+++ /dev/null
@@ -1,34 +0,0 @@
-&sum{x} = 1 :- &sum{ 1 : a } >= 0.
-a :- &sum{x} = 1.
-&sum(head){x} = 1 :- &sum(body){ 1 : a } >= 0.
-a :- '&sum(body){x} = 1'.
-
-def(x) :- &sum(head){x} = 1.
-'&sum(body){x} = 1' :- def(x), &sum(body){x} = 1.
-{&sum(body){x} = 1}.
-
-&sum(head){aux(0)} = 1 :- a.
-def(aux(0)) :- &sum(head){aux(0)} = 1.
-&sum(head){aux(0)} = 0 :- not a.
-def(aux(0)) :- &sum(head){aux(0)} = 0.
-{a} :- def(aux(0)).
-'&sum(body){aux(0)} >= 0' :- &sum(body){ 1 : a } >= 0.
-&sum(body){ 1 : a } >=0   :- '&sum(body){aux(0)} >= 0'.
-'&sum(body){aux(0)} >= 0' :- def(aux(0)), &sum(body){aux(0)} >= 0.
-{&sum(body){aux(0)} >= 0}.
-
-&sum(head){x} = 0      :- not def(x).
-&sum(head){aux(0)} = 0 :- not def(aux(0)).
-
-&sum(head){x} = 1   :- &sum(body){ 1 : a } >= 0.
-def(x)              :- &sum(head){x} = 1.
-'&sum(body){x} = 1' :- def(x), &sum(body){x} = 1.
-a :- '&sum(body){x} = 1'.
-&sum(head){aux(0)} = 1    :- a.
-'&sum(body){aux(0)} >= 0' :- def(aux(0)), &sum(body){aux(0)} >= 0.
-&sum(body){ 1 : a } >=0   :- '&sum(body){aux(0)} >= 0'.
-
-&sum(head){aux(0)} = 1 :- a.
-def(aux(0))            :- &sum(head){aux(0)} = 1.
-{a} :- def(aux(0)).
- a  :- '&sum(body){x} = 1'.
diff --git a/slides/listings.tex b/slides/listings.tex
deleted file mode 100644
index 8d2ae14..0000000
--- a/slides/listings.tex
+++ /dev/null
@@ -1,68 +0,0 @@
-% The language definitions below require the following packages:
-%
-%     \usepackage{courier}
-%     \usepackage{xcolor}
-%     \usepackage{relsize}
-%
-%     \input{listings}
-%     \renewcommand{\Underscore}{\textscale{1}{\textunderscore}}
-%
-% Without extra packages I had to provide an alternative underscore definition
-% to get decent looking underscores.
-%
-% As an alternative to courier, it is also possible to use the `lmodern`
-% package.
-%
-%     \usepackage[T1]{fontenc}
-%     \usepackage{lmodern}
-%     \usepackage{xcolor}
-%     \usepackage{relsize}
-%
-%     \input{listings}
-%
-% When the python or clingo language is given, tex code can be embedded
-% escaping it in `#( ... #)`, which is treated like a comment in Python.
-% Furthermore, for logic programs the character sequence is `%%` is not output.
-% This can be used to add labels at the end of lines. For example, in a logic
-% program one can write
-%
-%     H :- B.%%#( \label{lst:rule} #)
-%
-% to refer to the rule from the document without having to worry about changing
-% line numbers when refactoring. The annotated program will still be runnable
-% with clingo.
-
-\providecommand{\Underscore}{\textunderscore}
-
-\lstdefinelanguage{clingo}{%
-  basicstyle=\ttfamily,%
-  keywordstyle=[1]\bfseries,%
-  keywordstyle=[2]\bfseries,%
-  keywordstyle=[3]\bfseries,%
-  showstringspaces=false,%
-  literate={_}{\Underscore}1 {\%\%}{}0,%
-  escapeinside={\#(}{\#)},%
-  alsoletter={\#,\&},%
-  keywords=[1]{not,from,import,def,if,else,elif,return,while,break,and,or,for,in,del,and,class,with,as,is,yield,async},%
-  keywords=[2]{\#const,\#show,\#minimize,\#base,\#theory,\#count,\#external,\#program,\#script,\#end,\#heuristic,\#edge,\#project,\#show,\#sum},%
-  keywords=[3]{&,&dom,&sum,&diff,&show},%
-  morecomment=[l]{\#\ },%
-  morecomment=[l]{\%\ },%
-  morestring=[b]",%
-  stringstyle={\itshape},%
-  commentstyle={\color{darkgray}}%
-}
-
-\lstdefinelanguage{python}{%
-  basicstyle=\ttfamily,%
-  keywordstyle=[1]\bfseries,%
-  showstringspaces=false,%
-  literate={_}{\Underscore}{1},%
-  escapeinside={\#(}{\#)},%
-  alsoletter={\#,\&},%
-  keywords=[1]{not,from,import,def,if,else,elif,return,while,break,and,or,for,in,del,and,class,with,as,is,yield,async},%
-  morecomment=[l]{\#\ },%
-  morestring=[b]",%
-  stringstyle={\itshape},%
-  commentstyle={\color{darkgray}}%
-}
diff --git a/slides/macro.tex b/slides/macro.tex
deleted file mode 100644
index bfdeaee..0000000
--- a/slides/macro.tex
+++ /dev/null
@@ -1,172 +0,0 @@
-%!TEX root = paper.tex
-
-\newtheorem{proposition}{Proposition}
-\newcommand{\den}[1]{\llbracket \, #1 \, \rrbracket}
-% \newcommand{\denc}[3]{\llbracket \, #3 \, \rrbracket_{\langle#1,#2\rangle}}
-% \newcommand{\inter}[2]{\ensuremath{\mathcal{I}_{#1,#2}}}
-% \newcommand{\CC}{\ensuremath{\mathcal{C^+}}} % {\ensuremath{\mathcal{C_C}}} % {\ensuremath{\mathcal{CC}}}
-% \newcommand{\TC}[1]{\ensuremath{\mathcal{T_{#1}}}}
-% \newcommand{\cond}[2]{\ensuremath{|#1:#2|}}
-\newcommand{\ctermm}[3]{\ensuremath{{#1|#2}{:\,}#3}}
-\newcommand{\cterm}[3]{\ensuremath{(\ctermm{#1}{#2}{#3})}} % {\ensuremath{({#1|#2}\mathrel{:}#3})}
-% \newcommand{\ct}[1]{\ensuremath{\mathit{ct}(#1)}}
-% \newcommand{\cte}[2]{\ensuremath{\mathit{ct}_{\langle #1\rangle}(#2)}}
-\newcommand{\close}[1]{\ensuremath{#1\raisebox{1pt}{$\uparrow$}}}
-
-\newcommand{\htag}[2]{\ensuremath{\mathit{#1}\agg{#2}}}
-\newcommand{\htagg}[4]{\ensuremath{\mathit{#1}\agg{#2}\mathrel{#3}#4}}
-\newcommand{\htaggg}[4]{\ensuremath{\mathit{#1} {#2 }\mathrel{#3}#4}}
-\newcommand{\vals}[2]{\ensuremath{\mathcal{V}_{#1,#2}}}
-\newcommand{\eval}[2]{\ensuremath{\mathit{eval}}_{\langle #1,#2\rangle}}
-% \newcommand{\evalgz}[2]{\ensuremath{\mathit{eval}^{\gz}_{\langle #1,#2\rangle}}}
-% \newcommand{\evalf}[2]{\ensuremath{\mathit{eval}^{\f}_{\langle #1,#2\rangle}}}
-% \newcommand{\evals}[3]{\ensuremath{\mathit{eval}^{#1}_{\langle #2,#3\rangle}}}
-% \newcommand{\evalcl}[1]{\ensuremath{\mathit{eval}_{#1}}}
-
-\newcommand{\evalgz}[2]{\ensuremath{{\gz}_{\langle #1,#2\rangle}}}
-\newcommand{\evalf}[2]{\ensuremath{{\f}_{\langle #1,#2\rangle}}}
-\newcommand{\evals}[3]{\ensuremath{{#1}_{\langle #2,#3\rangle}}}
-\newcommand{\evalcl}[1]{\ensuremath{\mathit{eval}_{#1}}}
-\newcommand{\evall}[1]{\ensuremath{\mathit{eval}}_{#1}}
-\newcommand{\evallgz}[1]{\ensuremath{\mathit{eval}^{\mathtt{gz}}_{#1}}}
-
-\newcommand{\modelscl}{\ensuremath{\models_{cl}}}
-\newcommand{\eqdef}{%
-  \mathrel{\vbox{\offinterlineskip\ialign{%
-    \hfil##\hfil\cr%
-    $\scriptscriptstyle\mathrm{def}$\cr%
-    \noalign{\kern1pt}%
-    $=$\cr%
-    \noalign{\kern-0.1pt}%
-}}}}
-
-\newcommand{\sysfont}{\textit}
-\newcommand{\clingo}{\sysfont{clingo}}
-\newcommand{\clingcon}{\sysfont{clingcon}}
-\newcommand{\clingoDL}{\clingo{\small\textnormal{[}\textsc{DL}\textnormal{]}}}
-\newcommand{\dlprogram}{\textit{DL}-program}
-\newcommand{\code}[1]{\texttt{#1}}
-\newcommand{\ground}{variable-free}
-\newcommand{\modelsgz}{\models_{\gz}}
-\newcommand{\modelsf}{\models_{\f}}
-\newcommand{\modelss}{\models_{\sem}}
-\newcommand{\modelsp}[1]{\models_{#1}}
-\newcommand{\Atoms}{\mathit{Atoms}}
-\newcommand{\Head}{\mathit{H}}
-\newcommand{\HeadA}{\mathit{\Head_A}}
-\newcommand{\HeadB}{\mathit{\Head_B}}
-\newcommand{\Headp}{\mathit{\Head^+}}
-\newcommand{\Headn}{\mathit{\Head^-}}
-\newcommand{\Body}{\mathit{B}}
-\newcommand{\Bodyp}{\mathit{\Body^+}}
-\newcommand{\Bodyn}{\mathit{\Body^-}}
-\newcommand{\var}{\mathit{var}}
-\newcommand{\Cond}{\mathit{Cond}}
-\newcommand{\tuple}[1]{\langle #1 \rangle}
-\newcommand{\restr}[2]{{#1|}_{\hspace{-1pt}#2}}
-\newcommand{\df}[1]{\mathit{def}(#1)}
-\newcommand{\HTC}{\ensuremath{\mathit{HT}_{\!C}}} % {\mathit{HT}_C}
-\newcommand{\HT}{\ensuremath{\mathit{HT}}}
-\newcommand{\X}{\ensuremath{\mathcal{X}}}
-\newcommand{\D}{\ensuremath{\mathcal{D}}}
-\newcommand{\Du}{\ensuremath{\mathcal{D}_{\mathbf{u}}}}
-\newcommand{\T}{\ensuremath{\mathcal{T}}}
-\newcommand{\C}{\ensuremath{\mathcal{C}}}
-\newcommand{\ET}{\ensuremath{\mathcal{T}^e}}
-\newcommand{\BT}{\ensuremath{\mathcal{T}^b}}
-\newcommand{\BC}{\ensuremath{\mathcal{C}^b}}
-\newcommand{\Cgr}{\ensuremath{\mathcal{C}^*}}
-\newcommand{\F}{\ensuremath{\mathcal{F}}}
-\newcommand{\I}{\ensuremath{\mathcal{I}}}
-\newcommand{\V}{\ensuremath{\mathcal{V}}}
-%\newcommand{\P}{\ensuremath{\mathcal{P}}}
-\newcommand{\A}{\ensuremath{\mathcal{A}}}
-\newcommand{\Piref}[1]{\Pi_{\ref{#1}}}
-\newcommand{\vars}[1]{\ensuremath{\mathit{vars}(#1)}}
-\newcommand{\varsp}[1]{\ensuremath{\mathit{vars}^{a}(#1)}}
-\newcommand{\atoms}[1]{\ensuremath{\mathit{atoms}(#1)}}
-\newcommand{\At}[1]{\ensuremath{\mathit{At}(#1)}}
-\newcommand{\val}{\ensuremath{v}} % {V}
-% \newcommand{\t}{\ensuremath{\mathbf{t}}} % {\boldsymbol{t}}
-\newcommand{\gz}{\ensuremath{\mathit{vc}}} % {\boldsymbol{f}}
-\newcommand{\f}{\ensuremath{\mathit{df}}} % {\boldsymbol{f}}
-\newcommand{\ff}{\ensuremath{\mathit{F}}} % {\boldsymbol{f}}
-\newcommand{\undefined}{\ensuremath{\mathbf{u}}} % {\boldsymbol{u}}
-\newcommand{\sem}{\ensuremath{\kappa}} % {\boldsymbol{u}}
-\newcommand{\ass}[3]{#1 := #2 \, .. \, #3}
-\newcommand{\LC}{\ensuremath{\mathit{LC}}}
-\newcommand{\DF}{\ensuremath{\boldsymbol{D\hspace{-1.2pt}F}}} % {\mathbf{DF}}
-\newcommand{\agg}[1]{\ensuremath{\dot{\{}#1\dot{\}}}} % {\text{\"\{}#1\text{\"\}}}
-\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
-\newcommand{\LX}{\ensuremath{\mathbb{X}}}
-\newcommand{\HU}{\ensuremath{\mathbb{U}}}
-\newcommand{\Gra}{\ensuremath{\mathit{G}^a}}
-\newcommand{\Gr}{\ensuremath{\mathit{G}}}
-\newcommand{\Def}{\delta}
-\newcommand{\grsep}{\,\big|\hspace{-3pt}\big|\hspace{-3pt}\big|\,}
-\newcommand{\isint}[1]{\ensuremath{\mathit{int}(#1)}}
-
-
-
-
-\let\olditem\item
-\let\oldenumerate\enumerate
-\let\oldendenumerate\endenumerate
-\let\olditemize\itemize
-\let\oldenditemize\enditemize
-\newcommand{\deitemize}{%
-\def\itemize{\def\item{}}
-\def\enditemize{\let\item\olditem}
-\def\enumerate{\let\item\olditem\oldenumerate}
-\def\endenumerate{\oldendenumerate\def\item{}}
-}
-
-\newcommand{\reitemize}{%
-\def\itemize{\olditemize}
-\def\enditemize{\oldenditemize}
-}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% with bullets
-
-\newenvironment{Itemize}{\begin{itemize}[leftmargin=0pt]}{\end{itemize}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% without bullets
-
-\renewenvironment{Itemize}{\let\item\relax}{\let\item\olditemize}
-\renewenvironment{itemize}{\let\item\olditem\olditemize}{\oldenditemize\let\item\relax}
-\renewenvironment{enumerate}{\let\item\olditem\oldenumerate}{\oldendenumerate\let\item\relax}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-% Some aggregate names
-\def\sumf{\mathit{sum}}
-\newcommand\op{\mathit{op}}
-\newcommand\EX{\mathcal{EX}}
-
-\newcommand{\appendblank}{\ensuremath{\circ}}
-\newcommand\theory[2]{\tuple{#1,#2}}
-\newcommand{\aggs}{\mathit{agg}}
-\newcommand{\levels}{\ell}
-\newcommand{\level}[1]{\levels(#1)}
-\newcommand{\gzsemantics}{\mbox{\gz-semantics}\xspace}
-\newcommand{\fsemantics}{\mbox{\f-semantics}\xspace}
-\newcommand{\sequilibrium}{\mbox{\sem-equilibrium}\xspace}
-\newcommand{\gzequilibrium}{\mbox{\gz-equilibrium}\xspace}
-\newcommand{\fequilibrium}{\mbox{\f-equilibrium}\xspace}
-\newcommand{\sstable}{\mbox{\sem-stable}\xspace}
-\newcommand{\gzstable}{\mbox{\gz-stable}\xspace}
-\newcommand{\fstable}{\mbox{\f-stable}\xspace}
-\def\kmapping{selection function}
-\def\kmappings{{\kmapping}s}
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "paper"
-%%% End:
diff --git a/slides/slides.tex b/slides/slides.tex
deleted file mode 100644
index 40bd0d4..0000000
--- a/slides/slides.tex
+++ /dev/null
@@ -1,277 +0,0 @@
-\documentclass[11pt]{beamer}
-\usetheme{Warsaw}
-\usepackage[utf8]{inputenc}
-\usepackage{amsmath}
-\usepackage{amsthm}
-\usepackage{amsfonts}
-\usepackage{amssymb}
-\usepackage{stmaryrd}
-\usepackage{listings}
-\author[Cabalar et al.]{Pedro Cabalar and Jorge Fandinno and Torsten Schaub and Philipp Wanko}
-\title[Implementing $\mathit{HT}_C$ using CASP]{Implementing (part of) $\mathit{HT}_C$ using Constraint Answer Set Programming: A prototype}
-%\setbeamercovered{transparent}
-%\setbeamertemplate{navigation symbols}{}
-%\logo{}
-%\institute{}
-\date{}
-%\subject{}
-\begin{document}
-
-\input{macro}
-\input{listings}
-
-\begin{frame}
-\titlepage
-\end{frame}
-
-\begin{frame}{Recap}
-\begin{itemize}
-\item \emph{Logic of Here-and-There with Constraints (\HTC)} allows for capturing non-monotonic reasoning over arbitrary constraints involving \emph{constraint variables} and \emph{conditional expressions}
-\pause
-\item Flexible syntax, \emph{constraint atoms} are (infinite) strings of symbols that may refer to variables and domain elements
-\begin{align*}
-"x-y\leq d"\quad"a"\quad"\mathit{sum}\agg{ \, s_1, s_2, \dots \,  } = s_0"
-\end{align*}
-\vspace*{-.5cm}
-\pause
-\item Flexible semantics, \emph{denotations} assign constraint atoms sets of satisfying \emph{valuations}
-\begin{align*}
-  \den{x-y\leq d}
-  =
-  \{v\in\mathcal{V}\mid v(x),v(y), d\in \mathbb{Z}, v(x)-v(y)\leq d\}
-\end{align*}
-\end{itemize}
-\end{frame}
-
-\begin{frame}{Recap}
-\begin{itemize}
-\item \emph{Conditional constraint atoms} may contain \emph{conditional expressions} $(\ctermm{s}{s'}{\varphi})$
-\pause
-\item \emph{Evaluation function} replaces conditional expressions $\tau=(\ctermm{s}{s'}{\varphi})$:
-  \begin{align*}
-    \eval{h}{t}(\tau)
-    &=
-      \left\{
-      \begin{array}{ll}
-        s & \text{if } \langle h,t\rangle\models\varphi\\
-        s' & \text{if } \langle t,t\rangle \hspace{2pt}\not\models\varphi\\
-        \undefined & \text{otherwise}
-      \end{array}
-      \right.
-  \end{align*}
-\vspace*{-.5cm}
-\pause
-\item \emph{Interpretations} $\tuple{h,t}$ are pairs of valuations with $h\subseteq t$
-\pause
-\item Syntax, semantics of \emph{formulas} are standard \HT\ but for condition:
-$\langle h,t \rangle \models c \text{ if } h\in \den{\eval{h}{t}(c)}$
-\end{itemize}
-\end{frame}
-
-\begin{frame}{Motivation}
-\begin{align*}
-  \mathit{total}(R) := \mathit{sum}\agg{ \, \mathit{tax}(P) : \mathit{lives}(P,R) \,  } \ \leftarrow \ \mathit{region}(R)
-\end{align*}
-\pause
-\small\lstinputlisting[linerange={21-21},numbers=none,mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/taxes.lp}
-\quad
-\pause
-\begin{itemize}
-  \item Linear, modular translation to CASP using the \clingo\ Python API
-  \pause
-  \item Python version of \clingcon\ as solver
-  \pause
-  \item Bonus goal: implementation only by adding atoms and rules for each theory atom via the backend
-\end{itemize}
-\end{frame}
-
-\begin{frame}
-\tableofcontents
-\end{frame}
-
-\section{\HTC\ to \emph{CASP}: Syntactic and semantic differences}
-
-\begin{frame}{Input language}
-\scriptsize\lstinputlisting[mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/htc_lang.lp}
-\end{frame}
-
-\begin{frame}{Example}
-\scriptsize\lstinputlisting[linerange={13-29},mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/taxes.lp}
-\end{frame}
-
-\begin{frame}{Target language}
-\scriptsize\lstinputlisting[mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/cp_lang.lp}
-\end{frame}
-
-\begin{frame}{Semantic differences}
-  \begin{itemize}
-    \item \emph{CASP} does not allow variables to be undefined
-    \pause
-    \item \clingcon\ treats theory atoms in the body as \emph{strict, external} and theory atoms in the head as \emph{non-strict, defined}
-    \pause
-    \item \HTC\ stable models require values of variables to be \emph{founded}, variables may be undefined, no implicit choice for body atoms
-    \pause
-    \item
-    \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-    \pause
-    \begin{tabular}{ll}
-    \clingcon : & $\{\{(\mathtt{x},v)\} \mid v \ne 1 \} \cup \{\{\mathtt{a}, (\mathtt{x},1)\}\}$\\
-    \pause
-    \HTC      : & $\{\emptyset\}$
-    \end{tabular}
-    \pause
-    \item Add rules, sum constraints and auxiliary variables to implement constructs foreign to language of \clingcon
-  \end{itemize}
-\end{frame}
-
-
-\begin{frame}{Preprocessing: Seperate head from body}
-  \begin{itemize}
-    \item Use the abstract syntax tree to mark body and head theory atoms while parsing
-    \pause
-    \[
-\mathtt{\&}t\mathtt{\{}e_1:c_1,\dots,e_n:c_n\mathtt{\}} \prec k\pause \Rightarrow \mathtt{\&}t\mathtt{(}\mathit{l}\mathtt{)}\mathtt{\{}e_1:c_1,\dots,e_n:c_n\mathtt{\}}\prec k
-    \]
-    where $t$ is the name of the theory atom, $e_i$ are tuples of symbols, $c_i$ are conditions (both non-ground), $k$ is a theory term, $\prec$ is a relation symbol and $l\in\{\mathtt{head},\mathtt{body}\}$
-    \pause
-    \item
-    \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-    $\Rightarrow$
-    \lstinputlisting[linerange={2-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-  \end{itemize}
-\end{frame}
-
-\section{Founding variable values}
-
-\begin{frame}{Define variables}
-  \begin{itemize}
-    \item For every variable \texttt{x} occurring in the program, capture definedness with atom \texttt{def(x)} and add the rule
-\lstinputlisting[linerange={7-7},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-    \pause
-    \item For every condition-free linear constraint atom
-    \lstinputlisting[linerange={3-3},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-       add rule
-       \lstinputlisting[linerange={4-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-       for every $\mathtt{x} \in \vars{e_1}\cup\dots\cup\vars{e_n}\cup\vars{k}$
-   \end{itemize}
-\end{frame}
-
-\begin{frame}{Translating linear constraint atoms in the body}
-  For every condition-free linear constraint atom
-    \lstinputlisting[linerange={8-8},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-    \pause
-    \begin{itemize}
-      \item Copy the linear constraint and assign it to fresh atom
-           \pause
-      \item Do not communicate original linear constraint to \clingcon\ \pause
-      \item Add rules
-      \only<4>{\lstinputlisting[linerange={9-12},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}}
-      \only<5>{\lstinputlisting[linerange={13-15},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}}
-      where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_1}\cup\dots\cup\vars{e_n}\cup\vars{k}$
-    \end{itemize}
-\end{frame}
-
-\begin{frame}{Example}
-  We translate
-    \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}
-    \pause
-      to
-    \only<2>{\lstinputlisting[linerange={16-19},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}}
-    \only<3->{\lstinputlisting[linerange={20-23},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}}
-    \pause
-    \pause
-    \begin{tabular}{ll}
-    \clingcon : & $\{\{(x,0)\}\}$\\
-    \pause
-    \HTC      : & $\{\emptyset\}$
-    \end{tabular}
-\end{frame}
-
-\section{Translating conditional terms}
-\begin{frame}{Translating conditional terms}
-    \[
-\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k
-    \]
-    \vspace*{-.3cm}
-    \pause
-    \begin{itemize}
-  \item For every $e_i:c_i$, introduce auxiliary variable $\mathit{aux}_i$\pause\ and add following rules where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_i}$
-  \small\lstinputlisting[linerange={1-5},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/conditional.lp}
-  \pause
-  \item Replace conditional terms with respective auxiliary variables
-  \small\lstinputlisting[linerange={6-9},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/conditional.lp}
-    \end{itemize}
-\end{frame}
-
-\begin{frame}{Example: Vicious cycle}
-  \only<1>{\lstinputlisting[linerange={1-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}}
-  \only<2>{\scriptsize\lstinputlisting[linerange={3-21},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}}
-\end{frame}
-
-\begin{frame}{Example: Vicious cycle}
-  Value for \texttt{x} is unfounded due to loop through:
-  \scriptsize\lstinputlisting[linerange={23-30},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}
-\end{frame}
-
-\begin{frame}{Example: Vicious cycle}
-  Value for \texttt{aux(0)} is unfounded due to loop through:
-  \small\lstinputlisting[linerange={31-34},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}
-\end{frame}
-
-\section{Translating assignments, range, minimum/maximum constraint}
-\begin{frame}{Translating assignments and range constraints}
- \begin{itemize}
-    \item For assignment $\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} =: x$, we add
-    \pause
-    \lstinputlisting[linerange={1-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/assignments.lp}
-    where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_1}\cup\dots\cup\vars{e_n}$
-    \pause
-    \item For range constraint $\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$, we add
-    \pause
-    \lstinputlisting[linerange={3-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/assignments.lp}
- \end{itemize}
-\end{frame}
-
-\begin{frame}{Translating minimum constraints}
-\[\mathtt{\&min}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\]
-\pause
- \begin{itemize}
-    \item Add auxiliary variable $\mathit{min}$ and for every $e_i$, add following rules where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_i}$
-    \lstinputlisting[linerange={1-3},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp}
-    \pause
-    \item Check whether a correct value was selected
-    \lstinputlisting[linerange={4-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp}
-   \end{itemize}
-\end{frame}
-
-\begin{frame}{Translating minimum constraints}
-\[\mathtt{\&min}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\]
-\pause
- \begin{itemize}
-    \item If $l=\mathtt{body}$
-    \lstinputlisting[linerange={5-5},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp}
-    \pause
-    \item If $l=\mathtt{head}$
-    \lstinputlisting[linerange={6-7},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp}
- \end{itemize}
-\end{frame}
-
-\begin{frame}{Translating maximum constraints}
-\[\mathtt{\&max}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\]
-translates to
-\[\mathtt{\&min}(l)\mathtt{\{}-e_1,\dots,-e_n\mathtt{\}} \prec' -k\]
- \begin{itemize}
-    \item If $\prec=$ \texttt{<=}, $\prec'=$ \texttt{>=}
-    \item If $\prec=$ \texttt{>=}, $\prec'=$ \texttt{<=}
-    \item If $\prec=$ \texttt{<}, $\prec'=$ \texttt{>}
-    \item If $\prec=$ \texttt{>}, $\prec'=$ \texttt{<}
-    \item If $\prec=$ \texttt{=}, $\prec'=$ \texttt{=}
- \end{itemize}
-\end{frame}
-
-\section{Demonstration}
-\begin{frame}{Let's do our taxes!}
-  \huge\centering\textcolor{blue}{Demo}
-\end{frame}
-
-\end{document}
diff --git a/slides/slides.toc b/slides/slides.toc
deleted file mode 100644
index 94fd31c..0000000
--- a/slides/slides.toc
+++ /dev/null
@@ -1,5 +0,0 @@
-\beamer@sectionintoc {1}{\ensuremath {\mathit {HT}_{\tmspace -\thinmuskip {.1667em}C}}\ to \emph {CASP}: Syntactic and semantic differences}{15}{0}{1}
-\beamer@sectionintoc {2}{Founding variable values}{30}{0}{2}
-\beamer@sectionintoc {3}{Translating conditional terms}{42}{0}{3}
-\beamer@sectionintoc {4}{Translating assignments, range, minimum/maximum constraint}{50}{0}{4}
-\beamer@sectionintoc {5}{Demonstration}{61}{0}{5}