Logic and Modelling – Splitting

Splitting a formula is not like splitting an atom, haha :)

Splitting a formula is a way of checking the satisfiability of a propositional formula – or a set of formulas. The way we do this is by considering the truth values for Boolean variables occurring in the given formula, and then simplifying the formula depending on these values.
From these simplifications, we may even discover that we don’t always need to find the truth values for all Boolean variables in the formula.

Quick note. T = true (verum)               F = _|_ = false (falsum)

 

A Simple Example

Lets have a very basic example of the splitting method. Lets say we have the following formula:

• q /\ (p /\ q –> r) –> r

With this, lets say we want to ‘split’ on the Boolean variable ‘r’ first. In this case we make ‘r’ be true, so r=T:

• q /\ (p /\ q –> T) –> T

Now just simplify. But wait. isn’t anything that implies True… True? It sure is :D , so the simplified version of that whole formula is!

• T !!

Well that’s great, we didn’t even have to work out what ‘p’ and ‘q’ were :D

 

The Splitting Tree

The above method of splitting is okay, however there is a proper way to do it. We normally do splitting in the form of a tree. Lets take that same formula above, but this time negate it. So we have:

• ¬( q /\ (p /\ q –> r) –> r )

Now… if my theory is correct, that formula is unsatisfiable… in theory…
Either way, this is what the splitting tree looks like:

And, as you can see, i was correct :D

What the above image shows is what happens as you give a Boolean variable a value, simplify the resulting formula, and then split again.

So if we start at the top. When we make p=0, we replace all ‘p’ in the formula with ‘F’ (falsum). With this we simplify the formula to obtain “¬(q->r)”. Then say we make q=1, here we take the resultant simplified formula, and replace the ‘q’ with ‘T’ (verum). Simplifying gives us “¬(r)”. From this we just give ‘r’ either the value ‘1’ or ‘0’, and the result is the negation of the given value. So if r=0, the final result is ‘T’ (verum) :)

 

Note: this was a rather tricky post to make… if you see any mistakes, please do tell me! :D