Редукция ( лат. reductio — сведение, возведение, приведение обратно) — логический приём преобразования каких-либо данных к более удобному с какой-либо точки зрения виду; сведение сложного к более простому, доступному для анализа или решения.

Общее прототипическое значение — сокращение, уменьшение.

Правила редукции

конъюнкции ${\displaystyle [\land ]{\frac {\Gamma ,A\land B,\Delta }{\Gamma ,A,B,\Delta }}}$	отрицания конъюнкции ${\displaystyle [\neg \land ]{\frac {\Gamma ,\neg (A\land B),\Delta }{\Gamma ,\neg A,\Delta \mid \Gamma ,\neg B,\Delta }}}$	дизъюнкции ${\displaystyle [\lor ]{\frac {\Gamma ,A\lor B,\Delta }{\Gamma ,A,\Delta \mid \Gamma ,B,\Delta }}}$
отрицания дизъюнкции ${\displaystyle [\neg \lor ]{\frac {\Gamma ,\neg (A\lor B),\Delta }{\Gamma ,\neg A,\neg B,\Delta }}}$	импликации ${\displaystyle [\supset ]{\frac {\Gamma ,A\supset B,\Delta }{\Gamma ,\neg A,\Delta \mid \Gamma ,B,\Delta }}}$	отрицания импликации ${\displaystyle [\neg \supset ]{\frac {\Gamma ,\neg (A\supset B),\Delta }{\Gamma ,A,\neg B,\Delta }}}$
отрицания отрицания ${\displaystyle [\neg \neg ]{\frac {\Gamma ,\neg \neg A,\Delta }{\Gamma ,A,\Delta }}}$	квантора общности ${\displaystyle [\forall ]{\frac {\Gamma ,\forall xA(x),\Delta }{\Gamma ,\forall xA(x),A(t),\Delta }}}$	отрицания квантора общности ${\displaystyle [\neg \forall ]{\frac {\Gamma ,\neg \forall xA(x),\Delta }{\Gamma ,\neg A(k),\Delta }}}$
квантора существования ${\displaystyle [\exists ]{\frac {\Gamma ,\exists xA(x),\Delta }{\Gamma ,A(k),\Delta }}}$	отрицания квантора существования ${\displaystyle [\neg \exists ]{\frac {\Gamma ,\neg \exists xA(x),\Delta }{\Gamma ,\neg \exists xA(x),\neg A(t),\Delta }}}$	, где t — произвольный терм

В статье не хватает ссылок на источники (см. рекомендации по поиску ). Информация должна быть проверяема , иначе она может быть удалена. Вы можете статью, добавив ссылки на авторитетные источники в виде сносок . ( 14 мая 2011 )