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.

翻译：模演绎是一种通过计算规则而非公理来表达理论的方法。本文提出了一种模演绎的扩展，称为极化模演绎，在该框架中，部分规则仅能用于肯定出现的位置，而另一些规则仅能用于否定出现的位置。我们证明了命题演算中的所有理论都可以在此框架中表达，且此类理论中的切割总能被消去。