# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1384267246 0
# Node ID d35b2ee2e788b52523779d85890d950b056a8cda
# Parent  4e8482e505904c0d7ce36254a2f902a0dd62837b
add

diff -r 4e8482e50590 -r d35b2ee2e788 programs/prove2.scala
--- a/programs/prove2.scala	Tue Nov 12 10:51:02 2013 +0000
+++ b/programs/prove2.scala	Tue Nov 12 14:40:46 2013 +0000
@@ -1,5 +1,6 @@
 import scala.language.implicitConversions
 import scala.language.reflectiveCalls
+import scala.util._
 
 abstract class Term 
 case class Var(s: String) extends Term 
@@ -85,34 +86,32 @@
     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 => () }
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
 } 
 
+run (goal)
+
 run (Set[Form]() |- False -> Del)
 run (Set[Form]() |- True -> Del)
 run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
 
-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 f1 = Pred("F1", Nil)
+val f2 = Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
 
 
 val Chr = "Christian"
diff -r 4e8482e50590 -r d35b2ee2e788 progs/prove.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progs/prove.scala	Tue Nov 12 14:40:46 2013 +0000
@@ -0,0 +1,131 @@
+import scala.language.implicitConversions
+import scala.language.reflectiveCalls
+import scala.util._
+
+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, sc);
+    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
+  }
+}
+
+def prove1(j: Judgement, sc: () => Unit) : Unit = 
+  j.rhs match {
+    case True => sc ()
+    case False => ()
+    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, f1) => prove(j.lhs |- f1, sc) 
+    case Or(f1, f2) => 
+      { prove(j.lhs |- f1, sc);
+        prove(j.lhs |- f2, sc) }
+    case And(f1, f2) => 
+      prove(j.lhs |- f1, 
+            () => prove(j.lhs |- f2, sc))
+    case _ => ()
+  }
+
+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 = {
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
+} 
+
+run (goal)
+
+run (Set[Form]() |- False -> Del)
+run (Set[Form]() |- True -> Del)
+run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
+
+
+val Gamma1 : Set[Form] = 
+  Set( Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal1 = Gamma1 |- Del // not provable
+run (goal1)
+
+
+val f1 = "P" says Pred("F1", Nil)
+val f2 = "Q" says Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
+
+
+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)
+
+
diff -r 4e8482e50590 -r d35b2ee2e788 slides/slides06.pdf
Binary file slides/slides06.pdf has changed
diff -r 4e8482e50590 -r d35b2ee2e788 slides/slides06.tex
--- a/slides/slides06.tex	Tue Nov 12 10:51:02 2013 +0000
+++ b/slides/slides06.tex	Tue Nov 12 14:40:46 2013 +0000
@@ -606,7 +606,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}[c]
-\frametitle{Sudoku}
+\frametitle{BTW}
 
 Are there sudokus that cannot be solved?\pause