1 import scala.language.implicitConversions |
1 import scala.language.implicitConversions |
2 import scala.language.reflectiveCalls |
2 import scala.language.reflectiveCalls |
|
3 import scala.util._ |
3 |
4 |
4 abstract class Term |
5 abstract class Term |
5 case class Var(s: String) extends Term |
6 case class Var(s: String) extends Term |
6 case class Const(s: String) extends Term |
7 case class Const(s: String) extends Term |
7 case class Fun(s: String, ts: List[Term]) extends Term |
8 case class Fun(s: String, ts: List[Term]) extends Term |
83 prove(lhs_rest |- Says(p, f1), |
84 prove(lhs_rest |- Says(p, f1), |
84 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
85 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
85 case _ => () |
86 case _ => () |
86 } |
87 } |
87 |
88 |
88 |
|
89 |
|
90 // function that calls prove and returns immediately once a proof is found |
89 // function that calls prove and returns immediately once a proof is found |
91 def run (j : Judgement) : Unit = { |
90 def run (j : Judgement) : Unit = { |
92 try { |
91 def sc () = { println ("Yes!"); throw new Exception } |
93 def sc () = { println ("Yes!"); throw new Exception } |
92 Try(prove(j, sc)) getOrElse () |
94 prove(j, sc) |
|
95 } |
|
96 catch { case e: Exception => () } |
|
97 } |
93 } |
|
94 |
|
95 run (goal) |
98 |
96 |
99 run (Set[Form]() |- False -> Del) |
97 run (Set[Form]() |- False -> Del) |
100 run (Set[Form]() |- True -> Del) |
98 run (Set[Form]() |- True -> Del) |
101 run (Set[Form]() |- Del -> True) |
99 run (Set[Form]() |- Del -> True) |
|
100 run (Set[Form]() |- Del -> Del) |
|
101 run (Set[Form]() |- Del -> Or(False, Del)) |
102 |
102 |
103 run (goal) |
|
104 |
103 |
105 val Gamma1 : Set[Form] = |
104 val Gamma1 : Set[Form] = |
106 Set( Admin says ((Bob says Del) -> Del), |
105 Set( Admin says ((Bob says Del) -> Del), |
107 Bob says Del ) |
106 Bob says Del ) |
108 |
107 |
109 val goal1 = Gamma1 |- Del // not provable |
108 val goal1 = Gamma1 |- Del // not provable |
110 |
|
111 run (goal1) |
109 run (goal1) |
112 |
110 |
113 run (Set[Form]() |- (Del -> Del)) |
|
114 |
111 |
115 run (Set[Form]() |- (Del -> Or(False, Del))) |
112 val f1 = Pred("F1", Nil) |
|
113 val f2 = Pred("F2", Nil) |
|
114 run (Set[Form](And(f1, f2)) |- And(f2, f1)) |
116 |
115 |
117 |
116 |
118 val Chr = "Christian" |
117 val Chr = "Christian" |
119 val HoD = "Peter" |
118 val HoD = "Peter" |
120 val Email = Pred("may_btain_email", List(Const(Chr))) |
119 val Email = Pred("may_btain_email", List(Const(Chr))) |