1 |
1 |
2 abstract class Term |
2 abstract class Term |
3 case class Var(s: String) extends Term |
3 case class Var(s: String) extends Term |
4 case class Const(s: String) extends Term |
4 case class Const(s: String) extends Term |
5 case class Fun(s: String, ts: List[Term]) extends Term |
5 case class Fun(s: String, ts: List[Term]) extends Term |
6 |
6 |
7 abstract class Form |
7 abstract class Form { |
|
8 def -> (that: Form) = Imp(this, that) |
|
9 } |
8 case object True extends Form |
10 case object True extends Form |
9 case object False extends Form |
11 case object False extends Form |
10 case class Pred(s: String, ts: List[Term]) extends Form |
12 case class Pred(s: String, ts: List[Term]) extends Form |
11 case class Imp(f1: Form, f2: Form) extends Form |
13 case class Imp(f1: Form, f2: Form) extends Form |
12 case class Says(p: String, f: Form) extends Form |
14 case class Says(p: String, f: Form) extends Form |
22 val Bob = "Bob" |
24 val Bob = "Bob" |
23 val Del = Pred("del_file", Nil) |
25 val Del = Pred("del_file", Nil) |
24 |
26 |
25 |
27 |
26 val Gamma = |
28 val Gamma = |
27 List( Imp(Says(Admin, Del), Del), |
29 List( Says(Admin, Del) -> Del, |
28 Says(Admin, Imp(Says(Bob, Del), Del)), |
30 Says(Admin, Says(Bob, Del) -> Del), |
29 Says(Bob, Del) ) |
31 Says(Bob, Del) ) |
30 |
32 |
31 val goal = Judgement(Gamma, Del) // request: provable or not? |
33 val goal = Judgement(Gamma, Del) // request: provable or not? |
32 |
34 |
33 def prove(j: Judgement, sc: () => Unit) : Unit = { |
35 def prove(j: Judgement, sc: () => Unit) : Unit = { |
80 } |
82 } |
81 |
83 |
82 run (goal) |
84 run (goal) |
83 |
85 |
84 |
86 |
85 run (Judgement(Nil, Imp(Del, Del))) |
87 run (Judgement(Nil, Del -> Del)) |
86 |
88 |
87 val Chr = "Christian" |
89 val Chr = "Christian" |
88 val HoD = "Michael Luck" |
90 val HoD = "Michael Luck" |
89 val Email = Pred("may_btain_email", List(Const(Chr))) |
91 val Email = Pred("may_btain_email", List(Const(Chr))) |
90 val AtLib = Pred("is_at_library", List(Const(Chr))) |
92 val AtLib = Pred("is_at_library", List(Const(Chr))) |
91 val Chr_Staff = Pred("is_staff", List(Const(Chr))) |
93 val Chr_Staff = Pred("is_staff", List(Const(Chr))) |
92 |
94 |
93 val Policy_HoD = Imp(Says(HoD, Chr_Staff), Chr_Staff) |
95 val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff |
94 val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email) |
96 val Policy_Lib = And(Chr_Staff, AtLib) -> Email |
95 val HoD_says = Says(HoD, Chr_Staff) |
97 val HoD_says = Says(HoD, Chr_Staff) |
96 |
98 |
97 run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email)) |
99 run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email)) |
98 |
100 |
99 // consider the cases for true and false |
101 // consider the cases for true and false |