1 

     2 abstract class Term 

     3 case class Var(s: String) extends Term 

     4 case class Const(s: String) extends Term 

     5 case class Fun(s: String, ts: List[Term]) extends Term

     6 

     7 abstract class Form {

     8   def -> (that: Form) = Imp(this, that)

     9 }

    10 case object True extends Form

    11 case object False extends Form

    12 case class Pred(s: String, ts: List[Term]) extends Form

    13 case class Imp(f1: Form, f2: Form) extends Form

    14 case class Says(p: String, f: Form) extends Form 

    15 case class And(f1: Form, f2: Form) extends Form 

    16 case class Or(f1: Form, f2: Form) extends Form 

    17 

    18 case class Judgement(Gamma: List[Form], F: Form) {

    19   def lhs = Gamma

    20   def rhs = F

    21 }

    22 

    23 val Admin = "Admin"

    24 val Bob = "Bob"

    25 val Del = Pred("del_file", Nil)

    26 

    27 val Gamma = 

    28   List( Says(Admin, Del) -> Del,

    29         Says(Admin, Says(Bob, Del) -> Del),

    30         Says(Bob, Del) )

    31 

    32 val goal = Judgement(Gamma, Del) // request: provable or not?

    33 

    34 def partitions[A](ls: List[A]): List[(A, List[A])]  = 

    35   ls.map (s => (s, ls diff List(s)))

    36 

    37 

    38 def prove(j: Judgement, sc: () => Unit) : Unit = {

    39   if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 

    40   else prove1(j.lhs, j.rhs, sc) 

    41 }

    42 

    43 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 

    44   rhs match {

    45     case True => sc ()

    46     case False => ()

    47     case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 

    48     case Says(p, f1) => prove(Judgement(lhs, f1), sc) 

    49     case Or(f1, f2) => 

    50       { prove(Judgement(lhs, f1), sc);

    51         prove(Judgement(lhs, f2), sc) }

    52     case And(f1, f2) => 

    53       prove(Judgement(lhs, f1), 

    54             () => prove(Judgement(lhs, f2), sc))

    55     case _ => { for ((f, lhs_rest) <- partitions(lhs))

    56                   prove2(f, lhs_rest, rhs, sc) }

    57   }

    58 

    59 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 

    60   f match {

    61     case True => prove(Judgement(lhs_rest, rhs), sc)

    62     case False => sc()

    63     case And(f1, f2) =>

    64       prove(Judgement(f1::f2::lhs_rest, rhs), sc)

    65     case Imp(f1, f2) => 

    66       prove(Judgement(lhs_rest, f1), 

    67             () => prove(Judgement(f2::lhs_rest, rhs), sc))

    68     case Or(f1, f2) => 

    69       prove(Judgement(f1::lhs_rest, rhs), 

    70             () => prove(Judgement(f2::lhs_rest, rhs), sc))

    71     case Says(p, Imp(f1, f2)) => 

    72       prove(Judgement(lhs_rest, Says(p, f1)), 

    73             () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) 

    74     case _ => ()

    75   }

    76 

    77   

    78 

    79 // function that calls prove and returns immediately once a proof is found

    80 def run (j : Judgement) : Unit = {

    81   try { 

    82     def sc () = { println ("Yes!"); throw new Exception }

    83     prove(j, sc) 

    84   }

    85   catch { case e: Exception => () }

    86 } 

    87 

    88 run (Judgement (Nil, False -> Del))

    89 run (Judgement (Nil, True -> Del))

    90 run (Judgement (Nil, Del -> True))

    91 

    92 run (goal)

    93 

    94 val Gamma1 = 

    95   List( Says(Admin, Says(Bob, Del) -> Del),

    96         Says(Bob, Del) )

    97 

    98 val goal1 = Judgement(Gamma1, Del) // not provable

    99 

   100 run (goal1)

   101 

   102 run (Judgement(Nil, Del -> Del))

   103 

   104 run (Judgement(Nil, Del -> Or(False, Del)))

   105 

   106 

   107 val Chr = "Christian"

   108 val HoD = "Peter"

   109 val Email = Pred("may_btain_email", List(Const(Chr)))

   110 val AtLib = Pred("is_at_library", List(Const(Chr)))

   111 val Chr_Staff = Pred("is_staff", List(Const(Chr)))

   112 

   113 val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff

   114 val Policy_Lib = And(Chr_Staff, AtLib) -> Email

   115 val HoD_says = Says(HoD, Chr_Staff)

   116 

   117 run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))

   118 

   119