Введение
Конденсированное отрывание (правило D) — это метод вывода наиболее общего возможного заключения на основе двух формальных логических утверждений. Он был разработан ирландским логиком Кэру Мередитом в 1950-х годах и основан на работах Лукасевича. Джей. А. Калман доказал, что любое заключение, которое может быть получено последовательностью однородной подстановки (все вхождения переменной заменяются одним и тем же значением) и шагами modus ponens, может быть получено либо только конденсированным отрыванием, либо является результатом подстановки заключения, которое может быть получено только конденсированным отрыванием. Это делает конденсированное отрывание полезным для любой логической системы, обладающей modus ponens и подстановкой, независимо от того, является ли она D-полной.
D-нотация
Поскольку данная главная посылка и данная частная посылка однозначно определяют заключение (с точностью до переименования переменных), Мередит заметил, что достаточно лишь указать, какие два утверждения участвуют, и что сжатое отсечение можно использовать без каких-либо дополнительных обозначений. Это привело к созданию "D-нотации" для доказательств. Эта нотация использует оператор "D" для обозначения сжатого отсечения и принимает два аргумента в стандартной строке префиксной нотации. Например, если у вас есть четыре аксиомы, типичное доказательство в D-нотации может выглядеть так: DD12D34, что показывает шаг сжатого отсечения, использующий результат двух предыдущих шагов сжатого отсечения, первый из которых использовал аксиомы 1 и 2, а второй – аксиомы 3 и 4. Эта нотация, помимо использования в некоторых автоматических доказателях теорем, иногда встречается в каталогах доказательств. Например, база данных "самых коротких известных доказательств" проекта mmsolitaire в Metamath содержит 196 теорем с такими доказательствами. Использование сжатого отсечения с применением унификации предшествовало методу резолюции в автоматическом доказательстве теорем, который был представлен в 1965 году.
Преимущества
Для автоматизированного доказательства теорем конденсированное отсечение имеет ряд преимуществ по сравнению с прямым применением modus ponens и равномерной подстановкой. При доказательстве с использованием modus ponens и подстановки у вас есть бесконечное количество вариантов для подстановки вместо переменных. Это означает, что существует бесконечное количество возможных следующих шагов. В случае конденсированного отсечения количество возможных следующих шагов в доказательстве конечно. Обозначение D для полных доказательств конденсированного отсечения позволяет легко описывать доказательства для каталогизации и поиска. Типичное полное доказательство в 30 шагов занимает менее 60 символов в обозначении D (не считая формулировки аксиом).