1 import scala.language.implicitConversions

     2 import scala.language.reflectiveCalls

     3 

     4 abstract class Term 

     5 case class Var(s: String) extends Term 

     6 case class Const(s: String) extends Term 

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

     8 

     9 abstract class Form

    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: Set[Form], f: Form) {

    19   def lhs = gamma

    20   def rhs = f

    21 }

    22 

    23 // some syntactic sugar

    24 implicit def FormOps(f1: Form) = new {

    25   def -> (f2: Form) = Imp(f1, f2)

    26 }

    27 implicit def StringOps(p: String) = new {

    28   def says (f: Form) = Says(p, f)

    29 }

    30 implicit def SetFormOps(gamma: Set[Form]) = new {

    31   def |- (f: Form) : Judgement = Judgement(gamma, f)

    32 }

    33 

    34 val Admin = "Admin"

    35 val Bob = "Bob"

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

    37 

    38 val Gamma: Set[Form] = 

    39   Set( (Admin says Del) -> Del,

    40        (Admin says ((Bob says Del) -> Del)),

    41        (Bob says Del) )

    42 

    43 val goal = Gamma |- Del // request: provable or not?

    44 

    45 def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 

    46   s.map (e => (e, s - e))

    47 

    48 

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

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

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

    52 }

    53 

    54 def prove1(lhs: Set[Form], rhs: Form, sc: () => Unit) : Unit = 

    55   rhs match {

    56     case True => sc ()

    57     case False => ()

    58     case Imp(f1, f2) => prove(lhs + f1 |- f2, sc) 

    59     case Says(p, f1) => prove(lhs |- f1, sc) 

    60     case Or(f1, f2) => 

    61       { prove(lhs |- f1, sc);

    62         prove(lhs |- f2, sc) }

    63     case And(f1, f2) => 

    64       prove(lhs |- f1, 

    65             () => prove(lhs |- f2, sc))

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

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

    68   }

    69 

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

    71   f match {

    72     case True => prove(lhs_rest |- rhs, sc)

    73     case False => sc ()

    74     case And(f1, f2) =>

    75       prove(lhs_rest + f1 + f2 |- rhs, sc)

    76     case Imp(f1, f2) => 

    77       prove(lhs_rest |- f1, 

    78             () => prove(lhs_rest + f2 |- rhs, sc))

    79     case Or(f1, f2) => 

    80       prove(lhs_rest + f1 |- rhs, 

    81             () => prove(lhs_rest + f2 |- rhs, sc))

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

    83       prove(lhs_rest |- Says(p, f1), 

    84             () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 

    85     case _ => ()

    86   }

    87 

    88   

    89 

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

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

    92   try { 

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

    94     prove(j, sc) 

    95   }

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

    97 } 

    98 

    99 run (Set[Form]() |- False -> Del)

   100 run (Set[Form]() |- True -> Del)

   101 run (Set[Form]() |- Del -> True)

   102 

   103 run (goal)

   104 

   105 val Gamma1 : Set[Form] = 

   106   Set( Admin says ((Bob says Del) -> Del),

   107        Bob says Del )

   108 

   109 val goal1 = Gamma1 |- Del // not provable

   110 

   111 run (goal1)

   112 

   113 run (Set[Form]() |- (Del -> Del))

   114 

   115 run (Set[Form]() |- (Del -> Or(False, Del)))

   116 

   117 

   118 val Chr = "Christian"

   119 val HoD = "Peter"

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

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

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

   123 

   124 val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff

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

   126 val HoD_says = HoD says Chr_Staff

   127 

   128 run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)

   129 

   130