35 val Bob = "Bob" |
35 val Bob = "Bob" |
36 val Del = Pred("del_file", Nil) |
36 val Del = Pred("del_file", Nil) |
37 |
37 |
38 val Gamma: Set[Form] = |
38 val Gamma: Set[Form] = |
39 Set( (Admin says Del) -> Del, |
39 Set( (Admin says Del) -> Del, |
40 (Admin says ((Bob says Del) -> Del)), |
40 Admin says ((Bob says Del) -> Del), |
41 (Bob says Del) ) |
41 Bob says Del ) |
42 |
42 |
43 val goal = Gamma |- Del // request: provable or not? |
43 val goal = Gamma |- Del // request: provable or not? |
44 |
44 |
45 def partitions[A](s: Set[A]): Set[(A, Set[A])] = |
45 def partitions[A](s: Set[A]): Set[(A, Set[A])] = |
46 s.map (e => (e, s - e)) |
46 s.map (e => (e, s - e)) |
47 |
47 |
48 |
48 |
49 def prove(j: Judgement, sc: () => Unit) : Unit = { |
49 def prove(j: Judgement, sc: () => Unit) : Unit = { |
50 if (j.lhs.contains(j.rhs)) sc () // Axiom rule |
50 if (j.lhs.contains(j.rhs)) sc () // Axiom rule |
51 else prove1(j.lhs, j.rhs, sc) |
51 else prove1(j, sc) |
52 } |
52 } |
53 |
53 |
54 def prove1(lhs: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
54 def prove1(j: Judgement, sc: () => Unit) : Unit = |
55 rhs match { |
55 j.rhs match { |
56 case True => sc () |
56 case True => sc () |
57 case False => () |
57 case False => () |
58 case Imp(f1, f2) => prove(lhs + f1 |- f2, sc) |
58 case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) |
59 case Says(p, f1) => prove(lhs |- f1, sc) |
59 case Says(p, f1) => prove(j.lhs |- f1, sc) |
60 case Or(f1, f2) => |
60 case Or(f1, f2) => |
61 { prove(lhs |- f1, sc); |
61 { prove(j.lhs |- f1, sc); |
62 prove(lhs |- f2, sc) } |
62 prove(j.lhs |- f2, sc) } |
63 case And(f1, f2) => |
63 case And(f1, f2) => |
64 prove(lhs |- f1, |
64 prove(j.lhs |- f1, |
65 () => prove(lhs |- f2, sc)) |
65 () => prove(j.lhs |- f2, sc)) |
66 case _ => { for ((f, lhs_rest) <- partitions(lhs)) |
66 case _ => { for ((f, lhs_rest) <- partitions(j.lhs)) |
67 prove2(f, lhs_rest, rhs, sc) } |
67 prove2(f, lhs_rest, j.rhs, sc) } |
68 } |
68 } |
69 |
69 |
70 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
70 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
71 f match { |
71 f match { |
72 case True => prove(lhs_rest |- rhs, sc) |
72 case True => prove(lhs_rest |- rhs, sc) |