diff -r 4e8482e50590 -r d35b2ee2e788 programs/prove2.scala --- a/programs/prove2.scala Tue Nov 12 10:51:02 2013 +0000 +++ b/programs/prove2.scala Tue Nov 12 14:40:46 2013 +0000 @@ -1,5 +1,6 @@ import scala.language.implicitConversions import scala.language.reflectiveCalls +import scala.util._ abstract class Term case class Var(s: String) extends Term @@ -85,34 +86,32 @@ case _ => () } - - // function that calls prove and returns immediately once a proof is found def run (j : Judgement) : Unit = { - try { - def sc () = { println ("Yes!"); throw new Exception } - prove(j, sc) - } - catch { case e: Exception => () } + def sc () = { println ("Yes!"); throw new Exception } + Try(prove(j, sc)) getOrElse () } +run (goal) + run (Set[Form]() |- False -> Del) run (Set[Form]() |- True -> Del) run (Set[Form]() |- Del -> True) +run (Set[Form]() |- Del -> Del) +run (Set[Form]() |- Del -> Or(False, Del)) -run (goal) val Gamma1 : Set[Form] = Set( Admin says ((Bob says Del) -> Del), Bob says Del ) val goal1 = Gamma1 |- Del // not provable - run (goal1) -run (Set[Form]() |- (Del -> Del)) -run (Set[Form]() |- (Del -> Or(False, Del))) +val f1 = Pred("F1", Nil) +val f2 = Pred("F2", Nil) +run (Set[Form](And(f1, f2)) |- And(f2, f1)) val Chr = "Christian"