22 |
22 |
23 val Admin = "Admin" |
23 val Admin = "Admin" |
24 val Bob = "Bob" |
24 val Bob = "Bob" |
25 val Del = Pred("del_file", Nil) |
25 val Del = Pred("del_file", Nil) |
26 |
26 |
27 |
|
28 val Gamma = |
27 val Gamma = |
29 List( Says(Admin, Del) -> Del, |
28 List( Says(Admin, Del) -> Del, |
30 Says(Admin, Says(Bob, Del) -> Del), |
29 Says(Admin, Says(Bob, Del) -> Del), |
31 Says(Bob, Del) ) |
30 Says(Bob, Del) ) |
32 |
31 |
35 def prove(j: Judgement, sc: () => Unit) : Unit = { |
34 def prove(j: Judgement, sc: () => Unit) : Unit = { |
36 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
35 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
37 else prove1(j.lhs, j.rhs, sc) |
36 else prove1(j.lhs, j.rhs, sc) |
38 } |
37 } |
39 |
38 |
40 def partitions(ls: List[Form]): List[(Form, List[Form])] = |
39 def partitions[A](ls: List[A]): List[(A, List[A])] = |
41 ls.map (s => (s, ls - s)) |
40 ls.map (s => (s, ls - s)) |
42 |
41 |
43 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
42 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
44 rhs match { |
43 rhs match { |
|
44 case True => sc() |
|
45 case False => () |
45 case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) |
46 case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) |
46 case Says(p, f1) => prove(Judgement(lhs, f1), sc) |
47 case Says(p, f1) => prove(Judgement(lhs, f1), sc) |
47 case Or(f1, f2) => |
48 case Or(f1, f2) => |
48 { prove(Judgement(lhs, f1), sc); |
49 { prove(Judgement(lhs, f1), sc); |
49 prove(Judgement(lhs, f2), sc) } |
50 prove(Judgement(lhs, f2), sc) } |
54 prove2(f, lhs_rest, rhs, sc) } |
55 prove2(f, lhs_rest, rhs, sc) } |
55 } |
56 } |
56 |
57 |
57 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = |
58 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = |
58 f match { |
59 f match { |
|
60 case True => prove(Judgement(lhs_rest, rhs), sc) |
|
61 case False => sc() |
59 case And(f1, f2) => |
62 case And(f1, f2) => |
60 prove(Judgement(f1::f2::lhs_rest, rhs), sc) |
63 prove(Judgement(f1::f2::lhs_rest, rhs), sc) |
61 case Imp(f1, f2) => |
64 case Imp(f1, f2) => |
62 prove(Judgement(lhs_rest, f1), |
65 prove(Judgement(lhs_rest, f1), |
63 () => prove(Judgement(f2::lhs_rest, rhs), sc)) |
66 () => prove(Judgement(f2::lhs_rest, rhs), sc)) |
79 prove(j, sc) |
82 prove(j, sc) |
80 } |
83 } |
81 catch { case e: Exception => () } |
84 catch { case e: Exception => () } |
82 } |
85 } |
83 |
86 |
|
87 run (Judgement (Nil, False -> Del)) |
|
88 run (Judgement (Nil, True -> Del)) |
|
89 run (Judgement (Nil, Del -> True)) |
|
90 |
84 run (goal) |
91 run (goal) |
85 |
92 |
|
93 val Gamma1 = |
|
94 List( Says(Admin, Says(Bob, Del) -> Del), |
|
95 Says(Bob, Del) ) |
|
96 |
|
97 val goal1 = Judgement(Gamma1, Del) // not provable |
|
98 |
|
99 run (goal1) |
86 |
100 |
87 run (Judgement(Nil, Del -> Del)) |
101 run (Judgement(Nil, Del -> Del)) |
|
102 |
|
103 run (Judgement(Nil, Del -> Or(False, Del))) |
|
104 |
88 |
105 |
89 val Chr = "Christian" |
106 val Chr = "Christian" |
90 val HoD = "Michael Luck" |
107 val HoD = "Michael Luck" |
91 val Email = Pred("may_btain_email", List(Const(Chr))) |
108 val Email = Pred("may_btain_email", List(Const(Chr))) |
92 val AtLib = Pred("is_at_library", List(Const(Chr))) |
109 val AtLib = Pred("is_at_library", List(Const(Chr))) |