1 import scala.language.implicitConversions

     2 import scala.language.reflectiveCalls

     3 import scala.util._

     4 

     5 abstract class Term 

     6 case class Var(s: String) extends Term 

     7 case class Const(s: String) extends Term 

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

     9 

    10 abstract class Form

    11 case object True extends Form

    12 case object False extends Form

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

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

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

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

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

    18 

    19 case class Judgement(gamma: Set[Form], f: Form) {

    20   def lhs = gamma

    21   def rhs = f

    22 }

    23 

    24 // some syntactic sugar

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

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

    27 }

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

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

    30 }

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

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

    33 }

    34 

    35 val Admin = "Admin"

    36 val Bob = "Bob"

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

    38 

    39 val Gamma: Set[Form] = 

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

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

    42        Bob says Del )

    43 

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

    45 

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

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

    48 

    49 

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

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

    52   else prove1(j, sc) 

    53 }

    54 

    55 def prove1(j: Judgement, sc: () => Unit) : Unit = 

    56   j.rhs match {

    57     case True => sc ()

    58     case False => ()

    59     case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 

    60     case Says(p, f1) => prove(j.lhs |- f1, sc) 

    61     case Or(f1, f2) => 

    62       { prove(j.lhs |- f1, sc);

    63         prove(j.lhs |- f2, sc) }

    64     case And(f1, f2) => 

    65       prove(j.lhs |- f1, 

    66             () => prove(j.lhs |- f2, sc))

    67     case _ => { for ((f, lhs_rest) <- partitions(j.lhs))

    68                   prove2(f, lhs_rest, j.rhs, sc) }

    69   }

    70 

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

    72   f match {

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

    74     case False => sc ()

    75     case And(f1, f2) =>

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

    77     case Imp(f1, f2) => 

    78       prove(lhs_rest |- f1, 

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

    80     case Or(f1, f2) => 

    81       prove(lhs_rest + f1 |- rhs, 

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

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

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

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

    86     case _ => ()

    87   }

    88 

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

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

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

    92   Try(prove(j, sc)) getOrElse ()

    93 } 

    94 

    95 run (goal)

    96 

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

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

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

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

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

   102 

   103 

   104 val Gamma1 : Set[Form] = 

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

   106        Bob says Del )

   107 

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

   109 run (goal1)

   110 

   111 

   112 val f1 = Pred("F1", Nil)

   113 val f2 = Pred("F2", Nil)

   114 run (Set[Form](And(f1, f2)) |- And(f2, f1))

   115 

   116 

   117 val Chr = "Christian"

   118 val HoD = "Peter"

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

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

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

   122 

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

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

   125 val HoD_says = HoD says Chr_Staff

   126 

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

   128 

   129