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 case object True extends Form

     9 case object False extends Form

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

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

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

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

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

    15 

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

    17   def lhs = Gamma

    18   def rhs = F

    19 }

    20 

    21 val Admin = "Admin"

    22 val Bob = "Bob"

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

    24 

    25 

    26 val Gamma = 

    27   List( Imp(Says(Admin, Del), Del),

    28         Says(Admin, Imp(Says(Bob, Del), Del)),

    29         Says(Bob, Del) )

    30 

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

    32 

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

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

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

    36 }

    37 

    38 def partitions(ls: List[Form]): List[(Form, List[Form])]  = 

    39   ls.map (s => (s, ls - s))

    40 

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

    42   rhs match {

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

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

    45     case Or(f1, f2) => 

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

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

    48     case And(f1, f2) => 

    49       prove(Judgement(lhs, f1), 

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

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

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

    53   }

    54 

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

    56   f match {

    57     case And(f1, f2) =>

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

    59     case Imp(f1, f2) => 

    60       prove(Judgement(lhs_rest, f1), 

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

    62     case Or(f1, f2) => 

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

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

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

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

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

    68     case _ => ()

    69   }

    70 

    71   

    72 

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

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

    75   try { 

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

    77     prove(j, sc) 

    78   }

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

    80 } 

    81 

    82 run (goal)

    83 

    84 

    85 run (Judgement(Nil, Imp(Del, Del)))

    86 

    87 val Chr = "Christian"

    88 val HoD = "Michael Luck"

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

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

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

    92 

    93 val Policy_HoD = Imp(Says(HoD, Chr_Staff), Chr_Staff)

    94 val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email)

    95 val HoD_says = Says(HoD, Chr_Staff)

    96 

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

    98 

    99 // consider the cases for true and false