--- a/programs/prove1.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-
-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 {
-  def -> (that: Form) = Imp(this, that)
-}
-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( Says(Admin, Del) -> Del,
-        Says(Admin, Says(Bob, Del) -> Del),
-        Says(Bob, Del) )
-
-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 prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
-  rhs match {
-    case True => sc ()
-    case False => ()
-    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 True => prove(Judgement(lhs_rest, rhs), sc)
-    case False => sc()
-    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 (Judgement (Nil, False -> Del))
-run (Judgement (Nil, True -> Del))
-run (Judgement (Nil, Del -> True))
-
-run (goal)
-
-val Gamma1 = 
-  List( Says(Admin, Says(Bob, Del) -> Del),
-        Says(Bob, Del) )
-
-val goal1 = Judgement(Gamma1, Del) // not provable
-
-run (goal1)
-
-run (Judgement(Nil, Del -> Del))
-
-run (Judgement(Nil, 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 = Says(HoD, Chr_Staff) -> Chr_Staff
-val Policy_Lib = And(Chr_Staff, AtLib) -> Email
-val HoD_says = Says(HoD, Chr_Staff)
-
-run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))
-
-