Create a gist now

Instantly share code, notes, and snippets.

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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment