We have sequent calculus rules for our basic operators, i.e., negation, conjunction and disjunction. For any other operator like NAND, NOR, XOR, etc. you just have to think about possible ways to rewrite them using negation, conjunction and disjunction, and that will give you rules for the sequent calculus. For XOR, you can use the following rules which create only two subgoals:
- XOR_RIGHT (p xor q) <-> (!p|!q) & (p|q)
- XOR_LEFT (p xor q) <-> (p&!q) | (!p&q)
In the same way, you can also obtain rules for equivalence and the if-then-else operator.
