# HG changeset patch # User Christian Urban # Date 1351581102 0 # Node ID 8b44bd11429200d74d00682a4eda6a349cb31944 # Parent 2c772c82b13e4024041d09845725314ac0e51756 added slides diff -r 2c772c82b13e -r 8b44bd114292 programs/prove1.scala --- /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 diff -r 2c772c82b13e -r 8b44bd114292 slides06.pdf Binary file slides06.pdf has changed diff -r 2c772c82b13e -r 8b44bd114292 slides06.tex --- /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{ +\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{ +\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{ +\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{ +\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{ +\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{ +\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{ + \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{ +\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{ +\begin{frame}[c] +\frametitle{Proofs} + + + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\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{ + \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{ +\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{ +\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{ +\begin{frame}[c] + +\begin{center} +\Large +\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} +\end{center} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\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{ +\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{ +\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: +