diff -r 7aec0986b229 -r 8f142ae324e2 Slides/Slides3.thy
--- a/Slides/Slides3.thy	Tue Jul 13 14:37:28 2010 +0100
+++ b/Slides/Slides3.thy	Tue Jul 13 23:39:39 2010 +0100
@@ -131,7 +131,7 @@
   \begin{frame}<1>[c]
   \frametitle{Higher-Order Unification}
 
-  State of the art:
+  State of the art at the time:
 
   \begin{itemize}
   \item Lambda Prolog with full Higher-Order Unification\\ 
@@ -961,13 +961,19 @@
 
   \item The alternative rule
 
-  %\begin{center}\small
-  %\colorbox{cream}{
-  %\smath{\{a.t \eqprob b.t'\}\cup P \redu{\id} \{\swap{a}{c}\act t \eqprob \swap{b}{c}\act t', a \freshprob t'\} \cup P}}
-  %\end{center}
+  \begin{center}\small
+  \colorbox{cream}{
+  \begin{tabular}{@ {}l@ {}}
+  \smath{\{a.t \eqprob b.t'\}\cup P \redu{\id}}\\ 
+  \mbox{}\hspace{2cm}\smath{\{\swap{a}{c}\act t \eqprob 
+  \swap{b}{c}\act t', c \freshprob t, c \freshprob t'\} \cup P}
+  \end{tabular}}
+  \end{center}
  
-
-  leads to a more complicated notion of mgu.
+  leads to a more complicated notion of mgu.\medskip\pause
+  
+  \footnotesize
+  \smath{\{a.X \eqprob b.Y\} \redu{} (\{a\fresh Y, c\fresh Y\}, [X:=\swap{a}{c}\swap{b}{c}\act Y])}
   \end{itemize}
 
   \end{frame}}
@@ -1003,7 +1009,7 @@
   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
   {\color{darkgray}
   \begin{minipage}{9cm}\raggedright
-  {\bf Problem:} If we ask whether
+  {\bf One problem:} If we ask whether
   
   \begin{center}
   ?- type ([(x, T')], lam(x.Var(x)), T) 
@@ -1027,7 +1033,7 @@
   \begin{frame}<1->
   \frametitle{Equivariant Unification}
 
-  James Cheney
+  James Cheney proposed
 
   \begin{center}
   \colorbox{cream}{
@@ -1036,7 +1042,7 @@
   \end{center}\bigskip\bigskip
   \pause
 
-  He also showed that this is undecidable in general. :(
+  But he also showed this problem is undecidable\\ in general. :(
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -1054,7 +1060,14 @@
   Unfortunately this breaks the mgu-property:
 
   \begin{center}
-  
+  \smath{a.Z \eqprob X.Y.v(a)}
+  \end{center}
+
+  can be solved by
+
+  \begin{center}
+  \smath{[X:=a, Z:=Y.v(a)]} and
+  \smath{[Y:=a, Z:=Y.v(Y)]}
   \end{center}
 
   \end{frame}}
@@ -1064,7 +1077,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>
+  \begin{frame}<1>[c]
   \frametitle{HOPU vs. NOMU}
 
   \begin{itemize}
@@ -1073,7 +1086,7 @@
   \colorbox{cream}{\smath{HOPU \Rightarrow NOMU}} 
   \end{center}\bigskip
 
-  \item Levi\bigskip
+  \item Jordi Levy and Mateu Villaret established\bigskip
   \begin{center}
   \colorbox{cream}{\smath{HOPU \Leftarrow NOMU}} 
   \end{center}\bigskip
@@ -1123,10 +1136,12 @@
   \frametitle{Complexity}
 
   \begin{itemize}
-  \item Maribel Fernandez
+  \item Christiopher Calves and Maribel Fernandez showed first that
+  it is polynomial and then also quadratic
 
-  \item Levi 
-  
+  \item Jordi Levy and Mateu Villaret showed that it is quadratic
+  by a translation into a subset of NOMU and using ideas from
+  Martelli/Montenari.
   
   \end{itemize}
 
@@ -1143,14 +1158,18 @@
 
   \begin{itemize}
   \item Nominal Unification is a completely first-order 
-  language, but implements unification modulo $\alpha$.\medskip\pause
+  language, but implements unification modulo $\alpha$.
+  \textcolor{gray}{(verification\ldots Ramana Kumar and Michael Norrish)}
+  \medskip\pause
 
   \item NOMU has been applied in term-rewriting and
-  logic programming. I hope it will also be used in typing
+  logic programming. \textcolor{gray}{(Maribel Fernandez et 
+  al has a KB-completion procedure.)} 
+  I hope it will also be used in typing
   systems.\medskip\pause
 
   \item NOMU and HOPU are `equivalent' (it took a long time
-  and considerable time to find this out).\medskip\pause
+  and considerable research to find this out).\medskip\pause
   
   \item The question about complexity is still an ongoing 
   story.\medskip 
@@ -1168,7 +1187,7 @@
   \frametitle{
   \begin{tabular}{c}
   \mbox{}\\[23mm]
-  \alert{\LARGE Thank you very much}\\
+  \alert{\LARGE Thank you very much!}\\
   \alert{\Large Questions?}
   \end{tabular}}