xor two equations (exercise sheet 2 question1)

Question

how can we xor two equations? what is the general rule?

for example: 

f = !x0 & !x1 & !x2 | x3 & (x1 | x2) | x0 & !x2 & !x3
f' = !x0 & !x1 | x3

Answer 1

You mean who do we apply XOR on two formulas?

Well. In propositional logic, we put the XOR operator in between:

f XOR f' = (!x0 & !x1 & !x2 | x3 & (x1 | x2) | x0 & !x2 & !x3) XOR (!x0 & !x1 | x3)

The XOR operator can be written as CNF ( (f → ¬f') & (¬f → f') = (¬f | →f') & (f' | f)) or DNF (f&¬f' | ¬f&f').

With BDDs, we just create the BDDs for the formulas and then Apply(XOR, BDD1, BDD2).

Comments

I watched the video in which they explained we xor the two equations and create the BDD in order to find a counterexample to prove these two equations are not equivalent. But I don't understand how we apply the xor on these two equations and create the BDD from it!

---

Just like this. We write XOR in between the two formulas, and then we do what we'd do with any other formula (that we want to write as an ROBDD) as well. Variable by variable we do the Shanon decomposition, and write the result in an ROBDD.

Answer 2

It appears to me that is a misunderstanding. Let me try to clarify this. XOR is a boolean function, i.e., it expects two boolean values and maps these to another boolean value according to the truth table that defines the XOR function. 

We also have to distinguish equations from equivalences. If we have two boolean values phi and psi, we can consider phi<->psi as another boolean value, since the equivalence is also a boolean function that maps two boolean values to another boolean value. 

Equations as the ones mentioned here are different to equivalences since they are at a meta level where we speak about formulas. If we write f = a&b we mean that we abbreviate a&b by f and consider therefore f as a synonym for a&b. Oftentimes, we emphasize the definitional character of such equations by writing f := a&b.

Such equations are not boolean values and therefore we cannot apply XOR to the boolean equations. If that has been said like this, it is not perfectly correct. We is meant is to apply XOR to the two values f and f' which are defined by these equations which means the same as applying XOR to the right hand sides of these equations, since the names f and f' are seen as abbreviations of the right hand sides.