  Deduction modulo is a way to express a theory using computation rules instead
of axioms. We present in this paper an extension of deduction modulo, called
Polarized deduction modulo, where some rules can only be used at positive
occurrences, while others can only be used at negative ones. We show that all
theories in propositional calculus can be expressed in this framework and that
cuts can always be eliminated with such theories.
