equal
deleted
inserted
replaced
35 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
35 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
36 else prove1(j.lhs, j.rhs, sc) |
36 else prove1(j.lhs, j.rhs, sc) |
37 } |
37 } |
38 |
38 |
39 def partitions[A](ls: List[A]): List[(A, List[A])] = |
39 def partitions[A](ls: List[A]): List[(A, List[A])] = |
40 ls.map (s => (s, ls - s)) |
40 ls.map (s => (s, ls diff List(s))) |
41 |
41 |
42 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
42 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
43 rhs match { |
43 rhs match { |
44 case True => sc() |
44 case True => sc() |
45 case False => () |
45 case False => () |
102 |
102 |
103 run (Judgement(Nil, Del -> Or(False, Del))) |
103 run (Judgement(Nil, Del -> Or(False, Del))) |
104 |
104 |
105 |
105 |
106 val Chr = "Christian" |
106 val Chr = "Christian" |
107 val HoD = "Michael Luck" |
107 val HoD = "Peter" |
108 val Email = Pred("may_btain_email", List(Const(Chr))) |
108 val Email = Pred("may_btain_email", List(Const(Chr))) |
109 val AtLib = Pred("is_at_library", List(Const(Chr))) |
109 val AtLib = Pred("is_at_library", List(Const(Chr))) |
110 val Chr_Staff = Pred("is_staff", List(Const(Chr))) |
110 val Chr_Staff = Pred("is_staff", List(Const(Chr))) |
111 |
111 |
112 val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff |
112 val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff |