--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/programs/prove1.scala Tue Oct 30 07:11:42 2012 +0000
@@ -0,0 +1,99 @@
+
+abstract class Term
+case class Var(s: String) extends Term
+case class Const(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+
+case class Judgement(Gamma: List[Form], F: Form) {
+ def lhs = Gamma
+ def rhs = F
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+
+val Gamma =
+ List( Imp(Says(Admin, Del), Del),
+ Says(Admin, Imp(Says(Bob, Del), Del)),
+ Says(Bob, Del) )
+
+val goal = Judgement(Gamma, Del) // request: provable or not?
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+ if (j.lhs.contains(j.rhs)) sc() // Axiom rule
+ else prove1(j.lhs, j.rhs, sc)
+}
+
+def partitions(ls: List[Form]): List[(Form, List[Form])] =
+ ls.map (s => (s, ls - s))
+
+def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit =
+ rhs match {
+ case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc)
+ case Says(p, f1) => prove(Judgement(lhs, f1), sc)
+ case Or(f1, f2) =>
+ { prove(Judgement(lhs, f1), sc);
+ prove(Judgement(lhs, f2), sc) }
+ case And(f1, f2) =>
+ prove(Judgement(lhs, f1),
+ () => prove(Judgement(lhs, f2), sc))
+ case _ => { for ((f, lhs_rest) <- partitions(lhs))
+ prove2(f, lhs_rest, rhs, sc) }
+ }
+
+def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit =
+ f match {
+ case And(f1, f2) =>
+ prove(Judgement(f1::f2::lhs_rest, rhs), sc)
+ case Imp(f1, f2) =>
+ prove(Judgement(lhs_rest, f1),
+ () => prove(Judgement(f2::lhs_rest, rhs), sc))
+ case Or(f1, f2) =>
+ prove(Judgement(f1::lhs_rest, rhs),
+ () => prove(Judgement(f2::lhs_rest, rhs), sc))
+ case Says(p, Imp(f1, f2)) =>
+ prove(Judgement(lhs_rest, Says(p, f1)),
+ () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc))
+ case _ => ()
+ }
+
+
+
+// function that calls prove and returns immediately once a proof is found
+def run (j : Judgement) : Unit = {
+ try {
+ def sc () = { println ("Yes!"); throw new Exception }
+ prove(j, sc)
+ }
+ catch { case e: Exception => () }
+}
+
+run (goal)
+
+
+run (Judgement(Nil, Imp(Del, Del)))
+
+val Chr = "Christian"
+val HoD = "Michael Luck"
+val Email = Pred("may_btain_email", List(Const(Chr)))
+val AtLib = Pred("is_at_library", List(Const(Chr)))
+val Chr_Staff = Pred("is_staff", List(Const(Chr)))
+
+val Policy_HoD = Imp(Says(HoD, Chr_Staff), Chr_Staff)
+val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email)
+val HoD_says = Says(HoD, Chr_Staff)
+
+run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))
+
+// consider the cases for true and false
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides06.tex Tue Oct 30 07:11:42 2012 +0000
@@ -0,0 +1,435 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{proof}
+\usepackage{beamerthemeplainculight}
+\usepackage[T1]{fontenc}
+\usepackage[latin1]{inputenc}
+\usepackage{mathpartir}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage[absolute,overlay]{textpos}
+\usepackage{ifthen}
+\usepackage{tikz}
+\usepackage{courier}
+\usepackage{listings}
+\usetikzlibrary{arrows}
+\usetikzlibrary{positioning}
+\usetikzlibrary{calc}
+\usepackage{graphicx}
+
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+
+% Isabelle characters
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharbar}{\isamath{\mid}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isacharbraceleft}{\{}
+\renewcommand{\isacharbraceright}{\}}
+\renewcommand{\isacharless}{$\langle$}
+\renewcommand{\isachargreater}{$\rangle$}
+\renewcommand{\isasymsharp}{\isamath{\#}}
+\renewcommand{\isasymdots}{\isamath{...}}
+\renewcommand{\isasymbullet}{\act}
+
+
+
+\definecolor{javared}{rgb}{0.6,0,0} % for strings
+\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
+\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
+\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
+
+\lstset{language=Java,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+\lstdefinelanguage{scala}{
+ morekeywords={abstract,case,catch,class,def,%
+ do,else,extends,false,final,finally,%
+ for,if,implicit,import,match,mixin,%
+ new,null,object,override,package,%
+ private,protected,requires,return,sealed,%
+ super,this,throw,trait,true,try,%
+ type,val,var,while,with,yield},
+ otherkeywords={=>,<-,<\%,<:,>:,\#,@},
+ sensitive=true,
+ morecomment=[l]{//},
+ morecomment=[n]{/*}{*/},
+ morestring=[b]",
+ morestring=[b]',
+ morestring=[b]"""
+}
+
+\lstset{language=Scala,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+% beamer stuff
+\renewcommand{\slidecaption}{APP 06, King's College London, 29 October 2012}
+
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \LARGE Access Control and \\[-3mm]
+ \LARGE Privacy Policies (6)\\[-6mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ %\begin{center}
+ %\includegraphics[scale=1.3]{pics/barrier.jpg}
+ %\end{center}
+
+\normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Of$\!$fice: & S1.27 (1st floor Strand Building)\\
+ Slides: & KEATS (also homework is there)\\
+ \end{tabular}
+ \end{center}
+
+
+\end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{1st Week}
+
+\begin{itemize}
+\item What are hashes and salts?\bigskip\pause
+\item \ldots can be use to store securely data on a client, but
+you cannot make your protocol dependent on the
+presence of the data\bigskip\pause
+\item \ldots can be used to store and verify passwords
+
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{2nd Week}
+
+\begin{itemize}
+\item Buffer overflows\bigskip
+\item choice of programming language can mitigate or even eliminate this problem
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{3rd Week}
+
+\begin{itemize}
+\item defence in depth\bigskip
+\item privilege separation afforded by the OS
+\end{itemize}
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (0, 1.1) rectangle (1.2,2);
+ \draw (4.7,1) node {Internet};
+ \draw (0.6,1.7) node {\footnotesize Slave};
+ \draw[line width=1mm] (0, 0) rectangle (1.2,0.9);
+ \draw (0.6,1.7) node {\footnotesize Slave};
+ \draw (0.6,0.6) node {\footnotesize Slave};
+ \draw (0.6,-0.5) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] processes\end{tabular}};
+ \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}};
+
+ \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2);
+ \draw (-2.9,1.7) node {\footnotesize Monitor};
+
+ \draw[white] (1.7,1) node (X) {};
+ \draw[white] (3.7,1) node (Y) {};
+ \draw[red, <->, line width = 2mm] (X) -- (Y);
+
+ \draw[red, <->, line width = 1mm] (-0.4,1.4) -- (-1.4,1.1);
+ \draw[red, <->, line width = 1mm] (-0.4,0.6) -- (-1.4,0.9);
+
+ \end{tikzpicture}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{4th Week}
+
+\begin{itemize}
+\item voting\ldots has security requirements that are in tension with each other
+\begin{center}
+integrity vs ballot secrecy\\
+authentication vs enfranchisment
+\end{center}\bigskip
+
+\item electronic voting makes `whole sale' fraud easier as opposed to `retail attacks'
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{5th Week}
+
+\begin{itemize}
+\item access control logic\bigskip
+
+\item formulas
+\item judgements
+\item inference rules
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
+
+ Formulas
+
+ \begin{itemize}
+ \item[]
+
+ \begin{center}\color{blue}
+ \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
+ \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\
+ & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+Judgements
+
+\begin{itemize}
+\item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$}
+\end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Inference Rules}
+
+\begin{center}
+\bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\
+
+\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_2}}
+\qquad
+\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\
+
+\bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\
+
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F_2}
+ {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad
+ \Gamma \vdash P \,\text{says}\, F_1}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Proofs}
+
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{The Access Control Problem}
+
+
+\begin{center}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2);
+ \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
+ \draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}};
+ \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}};
+
+ \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1);
+ \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
+ \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2);
+
+ \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
+
+ \end{tikzpicture}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ Recall the following scenario:
+
+ \begin{itemize}
+ \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
+ should be deleted, then this file must be deleted.
+ \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
+ \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.
+ \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.
+ \end{itemize}\bigskip
+
+ \small
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\
+ \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
+ \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
+ \end{tabular}}\medskip
+
+ \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip
+
+\begin{center}
+\Large \bl{\infer{\Gamma, F\vdash F}{}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad
+\bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause
+
+\begin{enumerate}
+\item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause
+\item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove
+\begin{center}
+\bl{$\Gamma \vdash F_2$}
+\end{center}\bigskip\pause
+
+\item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption
+\bl{$F_2$}.\bigskip
+\begin{center}
+\bl{$F_2, \Gamma \vdash \text{Pred}$}
+\end{center}
+
+\end{enumerate}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+