Избыточное доказательство

В математической логике избыточное доказательство — это доказательство , имеющее подмножество, которое является более коротким доказательством того же результата. Другими словами, доказательство является избыточным, если оно содержит больше шагов доказательства, чем фактически необходимо для доказательства результата. Формально доказательство $\psi$ из $\kappa$ считается излишним, если существует другое доказательство $\psi ^{\prime }$ из $\kappa ^{\prime }$ такой, что $\kappa ^{\prime }\subseteq \kappa$ (т.е. $\kappa ^{\prime }\;{\text{subsumes}}\;\kappa$) и $|\psi ^{\prime }|<|\psi |$ где $|\varphi |$ количество узлов в $\varphi$.

Локальное резервирование

Доказательство, содержащее поддоказательство фигур (здесь опущены опорные точки). указывают, что резольвенты должны быть определены однозначно)

$(\eta \odot \eta _{1})\odot (\eta \odot \eta _{2}){\text{ or }}\eta \odot (\eta _{1}\odot (\eta \odot \eta _{2}))$

является локально избыточным.

Действительно, оба этих поддоказательства можно эквивалентно заменить более коротким поддоказательством. $\eta \odot (\eta _{1}\odot \eta _{2})$. В случае локальной избыточности пары избыточных выводов, имеющих один и тот же стержень, встречаются в доказательстве близко друг к другу. Однако избыточные выводы также могут происходить далеко друг от друга в доказательстве.

Следующее определение обобщает локальную избыточность, рассматривая выводы с одним и тем же центром, которые происходят в разных контекстах. Мы пишем $\psi \left[\eta \right]$ для обозначения контекста доказательства $\psi \left[-\right]$ с одним заполнителем, замененным дополнительным доказательством $\eta$.

Глобальное резервирование

Доказательство

$\psi [\psi _{1}[\eta \odot _{p}\eta _{1}]\odot \psi _{2}[\eta \odot _{p}\eta _{2}]]{\text{ or }}\psi [\psi _{1}[\eta \odot _{p}(\eta _{1}\odot \psi _{2}[\eta \odot _{p}\eta _{2}])]]$

потенциально (глобально) избыточно. Более того, оно (глобально) избыточно, если его можно переписать в одно из следующих более коротких доказательств:

$\psi [\eta \odot _{p}(\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}])]{\text{ or }}\eta \odot _{p}\psi [\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]]{\text{ or }}\psi [\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]].$

Пример

Доказательство

${\cfrac {{\cfrac {{\cfrac {\eta :\,p,q\,\,\,\,\eta _{1}:\,\neg p,r}{q,r}}p\,\,\,\,\,\,{\begin{array}{c}\\\eta _{3}:\,\neg q\end{array}}}{r}}q\,\,\,\,\,\,\,\,\,\,\,\,\,{\cfrac {{\cfrac {\eta \,\,\,\,\,\,\,\,\,\,\,\,\,\eta _{2}:\,\neg p,s,\neg r}{q,s,\neg r}}p\,\,\,\,{\begin{array}{c}\\\eta _{3}\end{array}}}{s,\neg r}}q}{\psi :\,s}}r$

является локально избыточным, поскольку является экземпляром первого шаблона в определении $((\eta \odot _{p}\eta _{1})\odot \eta _{3})\odot ((\eta \odot _{p}\eta _{2})\odot \eta _{3}).$

• Шаблон $\psi [\psi _{1}[\eta \odot _{p}\eta _{1}]\odot \psi _{2}[\eta \odot _{p}\eta _{2}]]$
• $\psi _{1}[-]=\psi _{2}[-]=\_\odot \eta _{3}{\text{ and }}\psi [-]=\_$

Но это не является глобально избыточным, поскольку термины замены согласно определению содержат $\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]$ во всех случаях и $\psi _{1}[\eta _{1}]\odot \psi _{2}[\eta _{2}]=(\eta _{1}\odot \eta _{3})\odot (\eta _{2}\odot \eta _{3})$ не соответствует доказательству. В частности, ни $\eta _{1}$ ни $\eta _{2}$ можно решить с помощью $\eta _{3}$, поскольку они не содержат буквальный $q$.

Второй образец потенциально глобально избыточных доказательств, появляющихся в определении глобальной избыточности, связан с хорошо известным понятие регулярности . Неформально доказательство является нерегулярным, если существует путь от узла к корню доказательства, такой, что литерал используется более одного раза в качестве опорного элемента на этом пути.