--- a/programs/prove1.scala Tue Nov 12 08:03:16 2013 +0000
+++ b/programs/prove1.scala Tue Nov 12 09:57:22 2013 +0000
@@ -31,17 +31,18 @@
val goal = Judgement(Gamma, Del) // request: provable or not?
+def partitions[A](ls: List[A]): List[(A, List[A])] =
+ ls.map (s => (s, ls diff List(s)))
+
+
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[A](ls: List[A]): List[(A, List[A])] =
- ls.map (s => (s, ls diff List(s)))
-
def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit =
rhs match {
- case True => sc()
+ case True => sc ()
case False => ()
case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc)
case Says(p, f1) => prove(Judgement(lhs, f1), sc)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/programs/prove2.scala Tue Nov 12 09:57:22 2013 +0000
@@ -0,0 +1,130 @@
+import scala.language.implicitConversions
+import scala.language.reflectiveCalls
+
+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: Set[Form], f: Form) {
+ def lhs = gamma
+ def rhs = f
+}
+
+// some syntactic sugar
+implicit def FormOps(f1: Form) = new {
+ def -> (f2: Form) = Imp(f1, f2)
+}
+implicit def StringOps(p: String) = new {
+ def says (f: Form) = Says(p, f)
+}
+implicit def SetFormOps(gamma: Set[Form]) = new {
+ def |- (f: Form) : Judgement = Judgement(gamma, f)
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+val Gamma: Set[Form] =
+ Set( (Admin says Del) -> Del,
+ (Admin says ((Bob says Del) -> Del)),
+ (Bob says Del) )
+
+val goal = Gamma |- Del // request: provable or not?
+
+def partitions[A](s: Set[A]): Set[(A, Set[A])] =
+ s.map (e => (e, s - e))
+
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+ if (j.lhs.contains(j.rhs)) sc () // Axiom rule
+ else prove1(j.lhs, j.rhs, sc)
+}
+
+def prove1(lhs: Set[Form], rhs: Form, sc: () => Unit) : Unit =
+ rhs match {
+ case True => sc ()
+ case False => ()
+ case Imp(f1, f2) => prove(lhs + f1 |- f2, sc)
+ case Says(p, f1) => prove(lhs |- f1, sc)
+ case Or(f1, f2) =>
+ { prove(lhs |- f1, sc);
+ prove(lhs |- f2, sc) }
+ case And(f1, f2) =>
+ prove(lhs |- f1,
+ () => prove(lhs |- f2, sc))
+ case _ => { for ((f, lhs_rest) <- partitions(lhs))
+ prove2(f, lhs_rest, rhs, sc) }
+ }
+
+def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit =
+ f match {
+ case True => prove(lhs_rest |- rhs, sc)
+ case False => sc ()
+ case And(f1, f2) =>
+ prove(lhs_rest + f1 + f2 |- rhs, sc)
+ case Imp(f1, f2) =>
+ prove(lhs_rest |- f1,
+ () => prove(lhs_rest + f2 |- rhs, sc))
+ case Or(f1, f2) =>
+ prove(lhs_rest + f1 |- rhs,
+ () => prove(lhs_rest + f2 |- rhs, sc))
+ case Says(p, Imp(f1, f2)) =>
+ prove(lhs_rest |- Says(p, f1),
+ () => prove(lhs_rest + Says(p, f2) |- 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 (Set[Form]() |- False -> Del)
+run (Set[Form]() |- True -> Del)
+run (Set[Form]() |- Del -> True)
+
+run (goal)
+
+val Gamma1 : Set[Form] =
+ Set( Admin says ((Bob says Del) -> Del),
+ Bob says Del )
+
+val goal1 = Gamma1 |- Del // not provable
+
+run (goal1)
+
+run (Set[Form]() |- (Del -> Del))
+
+run (Set[Form]() |- (Del -> Or(False, Del)))
+
+
+val Chr = "Christian"
+val HoD = "Peter"
+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 = (HoD says Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
+val HoD_says = HoD says Chr_Staff
+
+run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)
+
+
Binary file slides/slides06.pdf has changed
--- a/slides/slides06.tex Tue Nov 12 08:03:16 2013 +0000
+++ b/slides/slides06.tex Tue Nov 12 09:57:22 2013 +0000
@@ -704,12 +704,12 @@
\end{tabular}
\end{center}
-We are better be able to prove:
+We better be able to prove:
\begin{center}
\begin{tabular}{@{}ll@{}}
-(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
-(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
\end{tabular}
\end{center}
@@ -729,6 +729,38 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+I want to prove
+
+\begin{center}
+\bl{$\Gamma \vdash \text{del\_file}$}
+\end{center}\pause
+
+There is an inference rule
+
+\begin{center}
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}\pause
+
+So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause
+
+\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\
+So I can use the rule
+
+\begin{center}
+\bl{\infer{\Gamma, F \vdash F}{}}
+\end{center}
+
+\onslide<5>{\bf\alert{What is wrong with this?}}
+\hfill{\bf Done. Qed.}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}