\documentclass{slides}

\pagestyle{empty}

%\usepackage{exptrees}

\begin{document}
\begin{slide} \setlength\parskip{0.6\parskip}
\begin{center} \bfseries TACTICS \end{center}

\begin{itemize}
\item Derived rules, eg \ \ 
\begin{tabular}{c}
W $\vdash$ (X ; Z), (Y ; Z) \\
\hline W $\vdash$ (X, Y) ; Z
\end{tabular}
%{\ttfamily
%$?W |- ($?X; $?Z), ($?Y; $?Z) ==> $?W |- ($?X, $?Y); $?Z
%}
\item Single step display, eg \verb: disp_tac "-lR*@" : \\
takes
Q $\vdash$ (Y; * $\bullet$ R), (* S; * $\bullet$ R) \\
to
R $\vdash$ $\bullet$ * (* $\bullet$ Y; (Q, * (* S; * $\bullet$ R)))

\item Global search and replace, eg using distributivity of 
* and $\bullet$ over , and ; and eliminating ** and $\bullet$ $\bullet$ 
gives \\
R $\vdash$ $\bullet$ ($\bullet$ Y; ((* S; * $\bullet$ R), * Q)) \\
R $\vdash$ ((* R; $\bullet$ * S), $\bullet$ * Q); Y

\item Display, rule, undisplay, eg applying weakening rule to
\verb: "-L" : position gives \\
R $\vdash$ (* R; $\bullet$ * S); Y

This requires new rules, eg \\
\begin{tabular}{c}
X $\vdash$ A \hspace{1em} X $\vdash$ B \\
\hline
X $\vdash$ A \& B
\end{tabular}
for
\begin{tabular}{c}
X $\vdash$ A \hspace{1em} Y $\vdash$ B \\
\hline
X, Y $\vdash$ A \& B
\end{tabular}

\end{itemize}

\end{slide}
\begin{slide} \setlength\parskip{0.7\parskip}
\begin{center} \bfseries TACTICS, etc \end{center}

\begin{itemize}
\item matching primitive propositions, eg in \\
$\bullet$ (A, * (B, C)) $\vdash$ * ($\bullet$ B, D)

\item General Isabelle tactics \\
REP\_DET\_EXP, THENEXP
\item Automating the cut elimination procedure -- 
involves manipulating proof trees
\item Identity tactic \\[1.0ex]
\mbox{} \hfill
\begin{tabular}{c}
S $\vdash$ S \hspace{1.0em}
R $\vdash$ R \hspace{1.0em}
T $\vdash$ T 
\\ \hline 
S $\circ$ ($\smile$R $\lor$ $\neg$T) $\vdash$ 
S $\circ$ ($\smile$R $\lor$ $\neg$T)
\end{tabular}
\hfill \mbox{}
\item Structural to logical conversion \\[1.0ex]
\mbox{} \hfill
\begin{tabular}{c}
(Q $\circ$ R) \& S $\vdash$ W \\ \hline
(Q; R), S $\vdash$ W  
\end{tabular}
\hfill \mbox{} 

\end{itemize}

\end{slide}

\end{document}