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

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

Неофициальное описание

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

Сгущенный отряд идет еще дальше и говорит:
"При условии $p$ подразумевает $q$ , и учитывая $r$ , унификатор используйте $p$ и $r$ сделать $p$ и $r$ то же самое, затем используйте стандартное правило отделения».

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

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

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

Некоторые логики, такие как классическое исчисление высказываний , имеют набор определяющих аксиом со свойством «D-полноты». Если набор аксиом D-полный, то любая действительная теорема системы, включая все ее экземпляры подстановки (вплоть до переименования переменных), может быть порождена только путем сокращенного отделения. Например, если $p\rightarrow p$ является теоремой D-полной системы, конденсированное отделение может доказать не только эту теорему, но и ее пример замены $(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.

Это обозначение не только используется в некоторых автоматизированных средствах доказательства теорем, но и иногда появляется в каталогах доказательств. Например, база данных «кратчайших известных доказательств» проекта mmsolitaire компании Metamath содержит 196 теорем с такими доказательствами. ^[3]

Использование унификации в сжатом отрыве предшествовало технологии которая автоматического доказательства теорем, была введена в 1965 году. ^[4]^[5]

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

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

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

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

Ссылки

^ Перейти обратно: ^а ^б Дж. А. Кальман (декабрь 1983 г.). «Сжатая отстраненность как правило вывода». Студия Логика . 42 (4): 443–451. дои : 10.1007/BF01371632 . S2CID 121221548 .
^ Н. Мегилл и М. Бандер (март 1996 г.). «Слабая D-полная логика» (PDF) . Дж. Игпл . 4 (2): 215–225. CiteSeerX 10.1.1.100.6257 . дои : 10.1093/jigpal/4.2.215 .
^ «Кратчайшие известные доказательства теорем исчисления высказываний из Principia Mathematica» . Метаматематика . Проверено 9 сентября 2023 г.
^ К. А. Мередит и А. Н. Прайор (1963). «Заметки об аксиоматике исчисления высказываний» . Нотр-Дам Ж. Формальная логика . 4 (3): 171–187. дои : 10.1305/ndjfl/1093957574 .
^ Дж. А. Робинсон (1965). «Машинно-ориентированная логика, основанная на принципе разрешения» . Журнал АКМ . 12 (1): 23–41. дои : 10.1145/321250.321253 . S2CID 14389185 .

Хиндли, Дж. Роджер (1993), «Логики BCK и BCI, конденсированное отделение и 2-свойство» , Notre Dame Journal of Formal Logic , 34 (2): 231–250, doi : 10.1305/ndjfl/1093634655 , MR 1231287
Уильям МакКьюн и Ларри Вос (1992). «Эксперименты по автоматической дедукции с конденсированным отделением» (PDF) . В Д. Капуре (ред.). Учеб. 11-я Международная конференция по автоматизированному дедукции (CADE) . ЛНКС. Том. 607. Спрингер. стр. 209–223.

[Kalman1983-1] Перейти обратно: ^а ^б Дж. А. Кальман (декабрь 1983 г.). «Сжатая отстраненность как правило вывода». Студия Логика . 42 (4): 443–451. дои : 10.1007/BF01371632 . S2CID 121221548 .

[MegillBunder1996-2] Н. Мегилл и М. Бандер (март 1996 г.). «Слабая D-полная логика» (PDF) . Дж. Игпл . 4 (2): 215–225. CiteSeerX 10.1.1.100.6257 . дои : 10.1093/jigpal/4.2.215 .

[3] «Кратчайшие известные доказательства теорем исчисления высказываний из Principia Mathematica» . Метаматематика . Проверено 9 сентября 2023 г.

[MeredithP63-4] К. А. Мередит и А. Н. Прайор (1963). «Заметки об аксиоматике исчисления высказываний» . Нотр-Дам Ж. Формальная логика . 4 (3): 171–187. дои : 10.1305/ndjfl/1093957574 .

[Robinson65-5] Дж. А. Робинсон (1965). «Машинно-ориентированная логика, основанная на принципе разрешения» . Журнал АКМ . 12 (1): 23–41. дои : 10.1145/321250.321253 . S2CID 14389185 .

[1]

[2]

[3]

[4]

[5]