Semantic Tableaux in Less than 90 Lines of Scala

This week challenge for me was to write a code that can check a propositional logic formula like
(¬(p ⋀ q) ↔ (¬p  ∨ ¬q)) ∧ ( ¬r ∧ q)  and check if the formula is valid or satisfiable. A formula is valid when it is always true under any interpretations of all its atoms. A formula is satisfiable when there is some interpretation of its atoms that can make the proposition true.

The complete code for this post is available here.

Semantic Tableaux
For example, p ⋀ q is satisfiable, since if p and q are both true, then the formula is true. (p  ∨ ¬p)  ⋀ (q ∨ ¬q) is valid, because regardless the interpretation of p and q, the formula is always true.

One way to implement the satisfiability and validity check is by creating truth table. But, the use of truth table is always exponential in number of atoms. There is fortunately a simple technique to check the validity and satisfiability a propositional logic formula. The technique is called Semantic Tableaux. I need to get my logic book I used back to the time of 2nd year of university (Ben-Ari, 1992 ) to remind me how it works. Basically, there are 9 rules, 5 α rules, and 4 β rules.

The following are the 9 rules:

α Rules

α	α1	α2
¬ ¬A	A
A1 ∧ A2	A1	A2
¬(A1 ∨ A2)	¬A1	¬A2
¬(A1 → A2)	A1	¬A2
(A1 ↔ A2)	A1 → A2	A2 → A1

β Rules

β	β1	β2
B1 ∨ B2	B1	B2
¬(B1 ∧ B2)	¬B1	¬B2
B1 → B2	¬B1	B2
¬(B1 ↔ B2)	¬(B1 → B2)	¬(B2 → B1)

I will not explain the Semantic Tableaux algorithms in detail. You can check a more detail in (Ben-Ari ) or in (Issawi, 92). Here is an example of tableau creation for ¬(p ⋀ q) ↔ (¬p  ∨ ¬q) :

Code 
Ok, let's start coding now.  The target is to have the following application working:

object Run { 
    def main(args:Array[String]):Unit = { 
      import Formulas._ 
      val formula1 = (¬('r) ∧ 'q) ∧ (¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) )) 
      println(isSatisfiable(formula1) + "," + isValid(formula1)) // true, false 
 
      val formula2 = ¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) ) 
      println(isSatisfiable(formula2) + "," + isValid(formula2)) // true, true 
    } 
  }

I used a sealed class Formula to represent all formulas. Atom, Conjunction, Disjunction, Implication, Equivalence, and Xor are classes that extends the trait. In addition, I introduced class  ¬ to represent the negation. Here is how it looks like.

sealed abstract class Formula  
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

Note that Atom class takes a symbol as its property, so that it allows us to write Atom('p) for example.

I let the Formula class empty in the example above just to make the examples clear. The content of the class is actually the boolean operation to a formula, like ∧,∨, →, ↔, and ⊕. I benefit from Scala that allows special characters to be used as function name. Here is the class Formula looks like:

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) 
}

With this, we can write(Atom('p) → Atom('q)) ∨ Atom(r). Not bad, but better to have directly ('p → 'q) ∨ r . For that purpose, implicit comes to rescue:

implicit def symbolToAtom(sym:Symbol) = Atom(sym)

We can now define how the validity and satisfiability work. This code illustrates the example of the application for testing our program:

object Run { 
    def main(args:Array[String]):Unit = { 
      import Formulas._ 
      val formula1 = (¬('r) ∧ 'q) ∧ (¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) )) 
      println(isSatisfiable(formula1) + "," + isValid(formula1)) // true, false 
 
      val formula2 = ¬('p ∧ 'q) ↔ (¬('p) ∨ ¬('q) ) 
      println(isSatisfiable(formula2) + "," + isValid(formula2)) // true, true 
    } 
  }

Now let's see the implementation of the 9 rules (you remember 5 α rules, and 4 β rules ?). It's quite simple actually. An application of rule actually retuns a list of leaf, and a leaf is actually a list of formula. Here it is:

  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)) 
  }

Nothing should be surprising except the case f if isLiteral(f) => List(Set(f)).  Just disregard this line at the moment, it's only useful in semantic tableau generation. Another surprise maybe for the equivalence rules.  The two equivalence rules in the code above are actually equivalent to the one in the rule table (leave as an exercise :-) ). Note how close the rules definition to its coding implementation. Isn't it nice ?

The most interesting part is of course the implementation of semantic tableau generation. In this naive implementation, the semantic tableau generation is embarrassingly simple, barely 10 lines of codes.

    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)) 
    }

Although short, the code is actually very dense. As you can see, the generation of semantic tableau above uses an auxiliary method openLeaf that does exactly that: opening a leaf. Opening a leaf is a recursive function that stops when all formulas in the leaf is a literal. A literal is either an atom or a negation of an atom. The else part is much more complex. But here is the idea: for each formula in a leaf, we apply one of the 9 rules defined above. The result of the application is combined using the combine function above. This will end up with a list of Leaf. For each leaf, then we recursively calls openLeaf using flatMap. This may be unclear, but try to play with the codes, hopefully it'll be clearer.

Finally, we need to implement validity and satisfiability check. A formula is f said to be valid if the semantic tableau for ¬f is closed. A semantic tableau is closed when all its leaves are closed, and finally a leaf is closed when it contains a formula in form of p and ¬p. Here is the implementation:

    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

We're done.

Summary
In this post, I showed my weekend hacking to implement naive satisfiability and validity checking of a propositional formula using semantic tableau. The implementation uses intensively Scala concepts like operator overriding, implicit, and fold and flatMap. All this concepts are helpful to implement the semantic tableaux techniques in relatively short Scala codes (less than 90 lines).  The use of operator helps readibility of the implementation (imagine how it looks like if I didn't use operators ∧,∨, →, ↔, and ⊕).

Reference
Ben-Ari, M (1992) Mathematical Logic for Computer Science. Prentice Hall.