29 Says(Admin, Says(Bob, Del) -> Del), |
29 Says(Admin, Says(Bob, Del) -> Del), |
30 Says(Bob, Del) ) |
30 Says(Bob, Del) ) |
31 |
31 |
32 val goal = Judgement(Gamma, Del) // request: provable or not? |
32 val goal = Judgement(Gamma, Del) // request: provable or not? |
33 |
33 |
|
34 def partitions[A](ls: List[A]): List[(A, List[A])] = |
|
35 ls.map (s => (s, ls diff List(s))) |
|
36 |
|
37 |
34 def prove(j: Judgement, sc: () => Unit) : Unit = { |
38 def prove(j: Judgement, sc: () => Unit) : Unit = { |
35 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
39 if (j.lhs.contains(j.rhs)) sc() // Axiom rule |
36 else prove1(j.lhs, j.rhs, sc) |
40 else prove1(j.lhs, j.rhs, sc) |
37 } |
41 } |
38 |
42 |
39 def partitions[A](ls: List[A]): List[(A, List[A])] = |
|
40 ls.map (s => (s, ls diff List(s))) |
|
41 |
|
42 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
43 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = |
43 rhs match { |
44 rhs match { |
44 case True => sc() |
45 case True => sc () |
45 case False => () |
46 case False => () |
46 case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) |
47 case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) |
47 case Says(p, f1) => prove(Judgement(lhs, f1), sc) |
48 case Says(p, f1) => prove(Judgement(lhs, f1), sc) |
48 case Or(f1, f2) => |
49 case Or(f1, f2) => |
49 { prove(Judgement(lhs, f1), sc); |
50 { prove(Judgement(lhs, f1), sc); |