Instantly share code, notes, and snippets.

# anrizal06/Proposition.scala Created Sep 24, 2011

What would you like to do?
Naîve Semantic Tableau for Propositional Logic
 package propositional import scala.annotation.tailrec sealed abstract class Formula { def ∧(q:Formula) = Conjunction(this, q) def ∨(q:Formula) = Disjunction(this,q) def →(q:Formula) = Implication(this,q) def ↔(q:Formula) = Equivalence(this,q) def ⊕(q:Formula) = Xor(this, q) } case class Atom(symbol:Symbol) extends Formula case class Conjunction(p:Formula, q:Formula) extends Formula case class Disjunction(p:Formula, q:Formula) extends Formula case class Implication(p:Formula, q:Formula) extends Formula case class Equivalence(p:Formula, q:Formula) extends Formula case class Xor(p:Formula,q:Formula) extends Formula case class ¬(p:Formula) extends Formula object Formulas { implicit def symbolToAtom(sym:Symbol) = Atom(sym) type Leaf = Set[Formula] def applyRule(f:Formula):List[Leaf] = f match { case f if isLiteral(f) => List(Set(f)) case ¬(¬(a)) => List(Set(a)) case Conjunction(a,b) => List(Set(a,b)) case ¬(Disjunction(a,b)) => List(Set(¬(a), ¬(b))) case ¬(Implication(a,b)) => List(Set(a, ¬(b))) case Disjunction(a,b) => List(Set(a), Set(b)) case ¬(Conjunction(a,b)) => List(Set(¬(a)), Set(¬(b))) case (Implication(a,b)) => List(Set(¬(a)), Set(b)) case Equivalence(a,b) => List( Set(a,b) , Set(¬(a), ¬(b))) case ¬(Equivalence(a,b)) => List(Set(a,¬(b)),Set(¬(a), b)) } def isLiteral(f:Formula):Boolean = f match { case Atom(_) => true case ¬(Atom(_)) => true case _ => false } def semanticTableau(f:Formula):List[Leaf] = { def combine(rec:List[Leaf], f:Formula):List[Leaf] = for ( a <- applyRule(f); b <- rec) yield (a ++ b) def openLeaf(leaf:Leaf):List[Leaf] = if (leaf forall isLiteral) List(leaf) else leaf.foldLeft(List(Set.empty:Leaf))(combine) flatMap(openLeaf) openLeaf(Set(f)) } @tailrec def isClosedLeaf(f:Leaf):Boolean = { if (f.isEmpty) false else { (f.head match { case Atom(_) => f.tail.exists( _ == ¬(f.head)) case ¬(Atom(a)) => f.tail.exists( _ == Atom(a)) case _ => false }) || isClosedLeaf(f.tail) } } def isOpenLeaf(f:Leaf) = !isClosedLeaf(f) def isValid(f:Formula):Boolean = semanticTableau(¬(f)) forall isClosedLeaf def isSatisfiable(f:Formula):Boolean = semanticTableau(f) exists isOpenLeaf }