Конденсированная отслойка - Condensed detachment

Конденсированная отслойка (Правило D) - это метод нахождения наиболее общего возможного вывода на основе двух формальных логических утверждений, разработанный ирландским обществом. логик Кэрью Мередит в 1950-х годах и вдохновленные работами Лукасевич.^[1]

Неформальное описание

Правило непривязанности (часто называемое modus ponens ) говорит:
"При условии ${\displaystyle p}$ подразумевает ${\displaystyle q}$, и учитывая ${\displaystyle p}$, сделать вывод ${\displaystyle q}$."

Конденсированная отслойка идет еще дальше и говорит:
"При условии ${\displaystyle p}$ подразумевает ${\displaystyle q}$, и учитывая ${\displaystyle r}$, использовать объединитель из ${\displaystyle p}$ и ${\displaystyle r}$ сделать ${\displaystyle p}$ и ${\displaystyle r}$ то же самое, тогда используйте стандартное правило непривязанности ".

А замена А что применительно к ${\displaystyle p}$ производит ${\displaystyle t}$, и замена B что применительно к ${\displaystyle r}$ производит ${\displaystyle t}$, называются объединителями ${\displaystyle p}$ и ${\displaystyle r}$.

Различные унификаторы могут создавать выражения с различным числом свободные переменные. Некоторые возможные объединяющие выражения: экземпляры замены других. Если одно выражение является экземпляром замены другого (а не просто переименованием переменной), то это другое называется «более общим».

Если наиболее общий объединитель используется в сокращенном отрыве, то логическим результатом является наиболее общий вывод, который можно сделать в данном выводе с данным вторым выражением. Поскольку любой более слабый вывод, который вы можете получить, является экземпляром замены наиболее общего, на практике когда-либо использовалось не что иное, как самый общий объединитель.

Некоторые логики, например классические пропозициональное исчисление, имеют набор определяющих аксиом со свойством «D-полнота». Если набор аксиом является D-полным, то любая действительная теорема системы, включая все ее экземпляры подстановки (вплоть до переименования переменных), может быть сгенерирована только путем сокращенного отсоединения. Например, если ${\displaystyle p\rightarrow p}$ является теоремой D-полной системы, конденсированное отщепление может доказать не только эту теорему, но и ее пример подстановки ${\displaystyle (p\rightarrow p)\rightarrow (p\rightarrow p)}$ используя более длинное доказательство. Обратите внимание, что «D-полнота» - это свойство аксиоматической основы системы, а не внутреннее свойство самой логической системы.^[2]

Дж. А. Калман доказал, что любой вывод, который может быть получен последовательностью равномерной подстановки (все экземпляры переменной заменяются одним и тем же содержанием), и modus ponens шаги могут быть либо сгенерированы только с помощью конденсированного отсоединения, либо являются экземпляром замещения чего-то, что может быть сгенерировано только с помощью конденсированного отсоединения.^[1]Это делает сжатое отключение полезным для любой логической системы, имеющей modus ponens и замещение, независимо от того, является ли оно D-полным.

D-обозначение

Поскольку данная основная посылка и данная второстепенная посылка однозначно определяют вывод (вплоть до переименования переменных), Мередит заметил, что необходимо было только отметить, какие два утверждения были задействованы, и что сжатое отстранение может использоваться без каких-либо других требуемых обозначений. Это привело к "D-нотации" для доказательства. Это обозначение использует оператор «D» для обозначения сжатого отсоединения и принимает 2 аргумента в стандартном префиксная запись нить. Например, если у вас есть четыре аксиомы, типичное доказательство в D-нотации может выглядеть так: DD12D34, который показывает этап сокращенного отделения с использованием результата двух предыдущих этапов сжатого отделения, первый из которых использовал аксиомы 1 и 2, а второй из который использовал аксиомы 3 и 4.

Эти обозначения, помимо того, что используются в некоторых автоматических средствах доказательства теорем, иногда появляются в каталогах доказательств.

Использование объединения в конденсированной отстраненности предшествовало разрешающая способность методы автоматическое доказательство теорем.^{[нужна цитата ]}

Преимущества

Для автоматизированного доказательства теорем конденсированная отслойка имеет ряд преимуществ перед необработанной modus ponens и равномерная подмена.

В Modus Ponens и доказательстве замены у вас есть бесконечное количество вариантов того, чем вы можете заменить переменные. Это означает, что у вас есть бесконечное количество возможных следующих шагов. В случае с ограниченной непривязанностью существует только конечное число возможных следующих шагов доказательства.^{[требуется разъяснение ]}

D-нотация для полных сокращенных доказательств обособленности позволяет легко описывать доказательства для каталогизации и поиска. Типичное полное 30-шаговое доказательство имеет длину менее 60 символов в D-нотации (исключая формулировку аксиом).

Рекомендации

1. J.A. Кальман (декабрь 1983 г.). «Концентрированная непривязанность как правило вывода». Studia Logica. 42 (4): 443–451. Дои:10.1007 / BF01371632.
2. Н. Мегилл и М. Бундер (март 1996 г.). "Более слабая D-полная логика" (PDF). J. IGPL. 4 (2): 215–225. CiteSeerX  10.1.1.100.6257. Дои:10.1093 / jigpal / 4.2.215.

• Хиндли, Дж. Роджер (1993), «Логика BCK и BCI, конденсированная отслойка и 2-свойство», Журнал формальной логики Нотр-Дам, 34 (2): 231–250, Дои:10.1305 / ndjfl / 1093634655, МИСТЕР  1231287
• Уильям МакКьюн и Ларри Вос (1992). «Эксперименты по автоматическому дедуктивному вычету с сокращенной непривязанностью» (PDF). В Д. Капуре (ред.). Proc. 11-я Международная конференция по автоматизированному вычету (CADE). LNCS. 607. Springer. С. 209–223.