Basing Sequent Systems on Exclusive-Or

In the standard Gentzen-type systems for classical logic, the right hand side of a sequent is interpreted as the inclusive-or of its elements. In this paper we investigate what happens if the exclusive-or. is used instead. We provide corresponding analytic systems, and some of the decision procedures that are based on them. The latter are particularly efficient for the negation-equivalence fragment of classical logic.