[SMT-LIB] Multiarity XOR, IFF

[Sava Krstic]

Radu's "use" of XOR-associativity reminds me of my first "serious" 
encounter with XOR and symmetric difference. It's the following problem.

In any school,

   the number of students taking an odd number of courses is odd

   if and only if

   the number of courses taken by an odd number of students is odd

Enjoy!

Sava



Radu Grigore wrote:
> Given the booleans b1, ..., bn out of which exactly m are true we can read
>   (xor b1 ... bn) as meaning odd(m)
> and
>   (iff b1 ... bn) as meaning odd(m)=odd(n)
> 
> Both "meanings" are easy to remember. Having "iff" interpreted as a
> conjunction would be quite confusing to people who use its
> associativity.
> 
> Here is a naive way to "use the associativity." If we know (iff a b c)
> and (iff d e f g) and we can unify (a,b) with (d,f) using the
> substitution s then we can conclude (iff s(c) s(e) s(g)). The
> processing pattern is quite simple and one can imagine a small tool
> based on it. (Of course, the keyword "imagine" is important.)
> 
> I'm sure the following tautology must appear in the book by Gries,
> which was mentioned, but I'll still write it since it is cute :) and
> illustrates another place where associativity is "used":
>   (iff (and A B) (or A B) A B)
>