slides/src/slides.tex
changeset 74 9938ea8ed067
parent 73 271b2a5270c1
     1.1 --- a/slides/src/slides.tex	Fri Jul 22 23:11:53 2011 +0200
     1.2 +++ b/slides/src/slides.tex	Fri Jul 22 23:39:42 2011 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4  \newtheorem*{def:general automata}{Generalised automaton}
     1.5  \newtheorem*{def:general acceptance}{Acceptance}
     1.6  \newtheorem*{def:syntax}{Syntax}
     1.7 +\newtheorem*{def:derived syntax}{Derived connectives}
     1.8  \newtheorem*{def:program}{Program}
     1.9  \newtheorem*{def:program automaton}{System automaton}
    1.10  
    1.11 @@ -118,7 +119,16 @@
    1.12  \subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}
    1.13  }
    1.14  \only<2>{
    1.15 -\subfigure{\includegraphics[width=20pt,height=10pt]{images/intel2.jpg}}
    1.16 +\subfigure{\includegraphics[width=35pt,height=20pt]{images/sun.jpg}}
    1.17 +\subfigure{\includegraphics[width=20pt,height=20pt]{images/hp.jpg}}
    1.18 +\subfigure{\includegraphics[width=40pt,height=20pt]{images/siemens.jpg}}
    1.19 +\subfigure{\includegraphics[width=15pt,height=20pt]{images/att.jpg}}
    1.20 +%\subfigure{\includegraphics[width=20pt,height=20pt]{images/motorola.jpg}}
    1.21 +\subfigure{\includegraphics[width=20pt,height=20pt]{images/sgi.jpg}}
    1.22 +\subfigure{\includegraphics[width=25pt,height=20pt]{images/fujitsu.jpg}}
    1.23 +\subfigure{\includegraphics[width=20pt,height=18pt]{images/nec.jpg}}
    1.24 +\subfigure{\includegraphics[width=20pt,height=20pt]{images/intel2.jpg}}
    1.25 +\subfigure{\includegraphics[width=25pt,height=20pt]{images/ibm.jpg}}
    1.26  }
    1.27  \end{figure}
    1.28  \end{frame}
    1.29 @@ -166,6 +176,23 @@
    1.30  \item $\U$ reads \emph{until}.
    1.31  \end{itemize}
    1.32  \end{def:syntax}
    1.33 +
    1.34 +\visible<2>{
    1.35 +\begin{def:derived syntax}
    1.36 +Let $\varphi$ and $\psi$ be formulae:
    1.37 +\begin{multicols}{2}
    1.38 +\begin{itemize}
    1.39 +\item $\top \equiv p \lor \neg p$ for $p \in \Prop$
    1.40 +\item $\bot \equiv \neg \top$
    1.41 +\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
    1.42 +\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
    1.43 +\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
    1.44 +\item $\Diamond \varphi \equiv \top \U \varphi$
    1.45 +\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
    1.46 +\end{itemize}
    1.47 +\end{multicols}
    1.48 +\end{def:derived syntax}
    1.49 +}
    1.50  \end{frame}
    1.51  
    1.52  \begin{frame}
    1.53 @@ -527,7 +554,7 @@
    1.54  $\Downarrow$\\
    1.55  Automaton $\A_\varphi$ for $\varphi$\\
    1.56  \vspace{20pt}
    1.57 -\visible<2>{\textcolor{red}{On-the-fly methods} \`a la Gerth et al.}
    1.58 +\visible<2>{\textcolor{red}{On-the-fly method} \`a la Gerth et al.}
    1.59  \end{center}
    1.60  \end{frame}
    1.61