В математической логике и автоматического доказательстве , разрешение является правилом вывода , ведущего к опровержению теоремы, доказав методики предложений в логике высказываний и логике первого порядка . Другими словами, итеративное применение правила разрешения подходящим способом позволяет определить, является ли пропозициональная формула выполнимой, и доказать, что формула первого порядка невыполнима. Попытка доказать выполнимую формулу первого порядка как невыполнимую, может привести к незавершенным вычислениям; эта проблема не возникает в логике высказываний.
Правило разрешения восходит к Дэвису и Патнэму (1960); [1] однако их алгоритм требовал проверки всех основных экземпляров данной формулы. Этот источник комбинаторного взрыва был устранен в 1965 году с помощью синтаксического алгоритма унификации Джона Алана Робинсона , который позволял создавать экземпляры формулы во время доказательства «по требованию» настолько, насколько это было необходимо для сохранения полноты опровержения . [2]
Предложение, созданное правилом разрешения, иногда называют резольвентой .
Разрешение в логике высказываний
Правило разрешения
Правило разрешения в логике высказываний является единственным действительным правилом вывода , который производит новый пункт подразумеваемого два пунктов , содержащих дополнительные литералы. Буквальным является пропозициональная переменная или отрицание пропозициональной переменной. Два литерала называются дополнениями, если один является отрицанием другого (в дальнейшем считается дополнением к ). Результирующее предложение содержит все литералы, не имеющие дополнений. Формально:
где
Вышеупомянутое также можно записать как:
Предложение, созданное правилом разрешения, называется резольвентой двух входных предложений. Это принцип консенсуса, применяемый к статьям, а не к условиям. [3]
Когда два предложения содержат более одной пары дополнительных литералов, правило разрешения может применяться (независимо) для каждой такой пары; однако в результате всегда получается тавтология .
Modus ponens можно рассматривать как частный случай разрешения (однобуквенного предложения и двубуквенного предложения).
эквивалентно
Техника разрешения
В сочетании с алгоритмом полного поиска правило разрешения дает надежный и полный алгоритм для определения выполнимости пропозициональной формулы и, в более широком смысле, действительности предложения в соответствии с набором аксиом.
Этот метод разрешения использует доказательство от противного и основан на том факте, что любое предложение в логике высказываний может быть преобразовано в эквивалентное предложение в конъюнктивной нормальной форме . [4] Шаги следующие.
- Все предложения в базе знаний и отрицание предложения, которое нужно доказать ( гипотеза ), связаны конъюнктивно.
- Результирующее предложение преобразуется в конъюнктивную нормальную форму с конъюнктами, рассматриваемыми как элементы в наборе S предложений. [4]
- Например, рождает множество .
- Правило разрешения применяется ко всем возможным парам предложений, которые содержат дополнительные литералы. После каждого применения правила разрешения результирующее предложение упрощается за счет удаления повторяющихся литералов. Если предложение содержит дополнительные литералы, оно отбрасывается (как тавтология). Если нет, и если он еще не присутствует в наборе предложений S , он добавляется к S и рассматривается для дальнейших выводов разрешения.
- Если после применения разрешающего правила получается пустое предложение , исходная формула является невыполнимой (или противоречивой ), и, следовательно, можно сделать вывод, что исходная гипотеза следует из аксиом.
- Если, с другой стороны, пустое предложение не может быть получено, и правило разрешения не может быть применено для получения новых предложений, гипотеза не является теоремой исходной базы знаний.
Одним из примеров этого алгоритма является исходный алгоритм Дэвиса – Патнэма, который позже был переработан в алгоритм DPLL, который устранил необходимость явного представления резольвент.
В этом описании метода разрешения используется набор S в качестве базовой структуры данных для представления производных разрешения. Списки , деревья и ориентированные ациклические графы - другие возможные и распространенные альтернативы. Представления дерева более верны тому факту, что правило разрешения является двоичным. Вместе с последовательной нотацией для предложений представление в виде дерева также дает понять, как правило разрешения связано с частным случаем правила вырезания , ограниченным атомарными формулами вырезания. Однако древовидные представления не так компактны, как представления наборов или списков, потому что они явно показывают избыточные поддифференциации предложений, которые используются более одного раза при выводе пустого предложения. Представления графов могут быть такими же компактными по количеству разделов, как и представления списков, и они также хранят структурную информацию о том, какие разделы были разрешены для получения каждой резольвенты.
Простой пример
Проще говоря: предположим ложно. Для помещения быть правдой, должно быть правдой. В качестве альтернативы предположимправда. Для помещения быть правдой, должно быть правдой. Таким образом, независимо от лжи или правдивости, если верны обе посылки, то вывод правда.
Разрешение в логике первого порядка
Правило разрешения может быть обобщено на логику первого порядка следующим образом: [5]
где является наиболее общим объединитель из а также , а также а также не имеют общих переменных.
Пример
Положения а также можно применить это правило с как объединитель.
Здесь x - переменная, а b - постоянная.
Здесь мы видим, что
- Положения а также являются предпосылками вывода
- (резольвент посылки) - его заключение.
- Буквальный левый разрешенный литерал,
- Буквальный является правильным разрешенным литералом,
- - разрешенный атом или стержень.
- является наиболее общим объединителем разрешенных литералов.
Неформальное объяснение
В логике первого порядка, разрешение конденсируется традиционные силлогизмы из логического вывода до одного правила.
Чтобы понять, как работает разрешение, рассмотрим следующий пример силлогизма терминологической логики :
- Все греки европейцы.
- Гомер - грек.
- Следовательно, Гомер - европеец.
Или, в более общем смысле:
- Следовательно,
Чтобы преобразовать рассуждения с использованием техники разрешения, сначала предложения должны быть преобразованы в конъюнктивную нормальную форму (CNF). В этой форме вся количественная оценка становится неявной: универсальные кванторы для переменных ( X , Y , ...) просто опускаются, как они понимаются, в то время как переменные, определяемые количественно экзистенциально , заменяются функциями Сколема .
- Следовательно,
Итак, вопрос в том, как метод разрешения выводит последнее предложение из первых двух? Правило простое:
- Найдите два предложения, содержащие один и тот же предикат, где он отрицается в одном предложении, но не в другом.
- Выполните объединение двух предикатов. (Если объединение не удалось, значит, вы неправильно выбрали предикаты. Вернитесь к предыдущему шагу и повторите попытку.)
- Если какие-либо несвязанные переменные, которые были связаны в унифицированных предикатах, также встречаются в других предикатах в двух предложениях, замените их также их связанными значениями (терминами).
- Отбросьте унифицированные предикаты и объедините оставшиеся из двух предложений в новое предложение, к которому также присоединяется оператор «∨».
Чтобы применить это правило к приведенному выше примеру, мы обнаруживаем, что предикат P встречается в отрицательной форме
- ¬ P ( X )
в первом предложении и в неотрицательной форме
- P ( а )
во втором пункте. X - это несвязанная переменная, а a - это связанное значение (термин). Объединение двух производит замену
- X ↦ a
Отказ от унифицированных предикатов и применение этой замены к остальным предикатам ( в данном случае только Q ( X )) приводит к заключению:
- Q ( а )
В качестве другого примера рассмотрим силлогистическую форму
- Все критяне - островитяне.
- Все островитяне лжецы.
- Следовательно, все критяне лжецы.
Или, в более общем смысле,
- ∀ X P ( X ) → Q ( Х )
- ∀ Икс Q ( X ) → R ( X )
- Следовательно, ∀ X P ( X ) → R ( X )
В CNF предшественниками становятся:
- ¬ P ( X ) ∨ Q ( X )
- ¬ Q ( Y ) ∨ R ( Y )
(Обратите внимание, что переменная во втором предложении была переименована, чтобы было ясно, что переменные в разных предложениях различны.)
Теперь объединение Q ( X ) в первом предложении с ¬ Q ( Y ) во втором предложении означает, что X и Y в любом случае становятся одной и той же переменной. Подставляя это в остальные предложения и объединяя их, можно сделать вывод:
- ¬ P ( X ) ∨ R ( X )
Факторинг
Правило разрешения, как определено Робинсоном, также включает факторинг, который объединяет два литерала в одном предложении до или во время применения разрешения, как определено выше. Результирующее правило вывода является полным опровержением [6] в том смысле, что набор предложений является неудовлетворительным тогда и только тогда, когда существует вывод пустого предложения с использованием только разрешения, усиленного факторизацией.
Примером набора невыполнимых предложений, для которого факторинг необходим для получения пустого предложения, является:
Поскольку каждое предложение состоит из двух литералов, то же самое и с каждой возможной резольвентой. Следовательно, при разрешении без факторизации пустое предложение никогда не может быть получено. Используя факторинг, можно получить, например, следующее: [7]
Неклаузальное разрешение
Были разработаны обобщения вышеупомянутого правила разрешения, которые не требуют, чтобы исходные формулы были в клаузальной нормальной форме . [8] [9] [10] [11] [12] [13]
Эти методы полезны в основном при интерактивном доказательстве теорем, где важно сохранить удобочитаемость формул промежуточных результатов для человека. Кроме того, они избегают комбинаторного взрыва при преобразовании в форму предложения, [10] : 98 и иногда сохраняют шаги разрешения. [13] : 425
Неклаузальное разрешение в логике высказываний
Для логики высказываний Мюррей [9] : 18 и Манна и Уолдингер [10] : 98 используют правило
- ,
где обозначает произвольную формулу, обозначает формулу, содержащую как подформула, и построен путем замены в каждое появление от ; аналогично для. Резольвента предназначен для упрощения с использованием таких правил, как и т. д. Чтобы предотвратить создание бесполезных тривиальных резольвент, правило должно применяться только тогда, когда имеет по крайней мере одно «отрицательное» и «положительное» [14] вхождение в а также , соответственно. Мюррей показал, что это правило является полным, если оно дополнено соответствующими правилами логического преобразования. [10] : 103
Трауготт использует правило
- ,
где показатели указать полярность его возникновения. Пока а также строятся по-прежнему, формула получается заменой каждого положительного и каждого отрицательного вхождения в с участием а также , соответственно. Подобно подходу Мюррея, к резольвенте необходимо применить соответствующие упрощающие преобразования. Трауготт доказал полноту своего правила при условии, что- единственные связки, используемые в формулах. [12] : 398–400
Решимость Трауготта сильнее, чем у Мюррея. [12] : 395 Более того, он не вводит новых бинарных соединителей, тем самым избегая тенденции к клаузальной форме при многократном разрешении. Однако формулы могут стать длиннее, если небольшая заменяется несколько раз на более крупный и / или . [12] : 398
Пример пропозициональной неклаузальной резолюции
В качестве примера, исходя из пользовательских предположений
Правило Мюррея можно использовать следующим образом, чтобы вывести противоречие: [15]
С той же целью можно использовать правило Трауготта следующим образом: [12] : 397
При сравнении обоих выводов можно увидеть следующие проблемы:
- Правило Трауготта может дать более точную резольвенту: сравните (5) и (10), которые оба разрешают (1) и (2) на .
- Правило Мюррея ввело 3 новых символа дизъюнкции: в (5), (6) и (7), в то время как правило Трауготта не вводило никаких новых символов; в этом смысле промежуточные формулы Трауготта больше напоминают стиль пользователя, чем стиль Мюррея.
- Из-за последней проблемы правило Трауготта может использовать импликацию в предположении (4), используя в качестве неатомическая формула на шаге (12). Используя правила Мюррея, семантически эквивалентная формула был получен как (7), однако его нельзя было использовать в качестве из-за его синтаксической формы.
Неклаузальное разрешение в логике первого порядка
Для логики предикатов первого порядка правило Мюррея обобщено, чтобы разрешить отдельные, но унифицированные подформулы а также из а также , соответственно. Если является наиболее общим объединителем а также , то обобщенная резольвента . Хотя правило остается в силе, если более специальная заменаиспользуется, такие приложения правил не требуются для достижения полноты. [ необходима цитата ]
Правило Трауготта обобщено, чтобы разрешить несколько попарно различных подформул из а также из , так долго как иметь общий самый общий объединитель, скажем . Обобщенная резольвента получается после примененияк родительским формулам, таким образом делая пропозициональную версию применимой. Доказательство полноты Трауготта основывается на предположении, что используется это полностью общее правило; [12] : 401 неясно, останется ли его правило полным, если ограничится а также . [16]
Парамодуляция
Парамодуляция - это связанный метод рассуждений о наборах предложений, в которых символом предиката является равенство. Он генерирует все «равные» версии предложений, кроме рефлексивных тождеств. Операция парамодуляции принимает положительное значение from , которое должно содержать литерал равенства. Затем он ищет предложение into с подтермином, которое объединяется с одной стороной равенства. Затем подтермин заменяется другой частью равенства. Общая цель парамодуляции - уменьшить систему до атомов, уменьшая размер термов при замене. [17]
Реализации
- КАРИН
- GKC
- Выдра
- Доказатель9
- СНАРК
- СПАСС
- Вампир
Смотрите также
- Конденсированная отслойка - более ранняя версия разрешения
- Индуктивное логическое программирование
- Обратное разрешение
- Логическое программирование
- Метод аналитических таблиц
- Разрешение SLD
- Вывод разрешения
Заметки
- ^ Мартин Дэвис, Хилари Патнэм (1960). «Вычислительная процедура для теории количественной оценки». J. ACM . 7 (3): 201–215. DOI : 10.1145 / 321033.321034 .Здесь: стр. 210, «III. Правило исключения атомных формул».
- ^ Дж. А. Робинсон (январь 1965 г.). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23–41. DOI : 10.1145 / 321250.321253 .
- ^ DE Knuth, Искусство компьютерного программирования 4A : комбинаторные алгоритмы , часть 1, стр. 539
- ^ а б Leitsch, Alexander (1997), Исчисление разрешающей способности, Монографии EATCS по теоретической информатике, Springer, стр. 11.
Перед применением самого метода вывода мы преобразуем формулы в бескванторную конъюнктивную нормальную форму.
- ^ Энрике П. Арис, Хуан Л. Гонсалеса у Фернандо М. Рубио, Logica Computacional, Thomson (2005).
- ^ Стюарт Дж. Рассел; Питер Норвиг (2009). Искусственный интеллект: современный подход (3-е изд.). Прентис Холл.п. 350 (= стр.286 в 1-м издании 1995 г.)
- ^ Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем . Нью-Йорк: Вили.См. Стр. 77. Пример здесь немного изменен, чтобы продемонстрировать нетривиальную замену факторинга. Для ясности шаг факторинга (5) показан отдельно. На шаге (6) новая переменная был введен для обеспечения унифицируемости (5) и (6), необходимой для (7).
- ^ Д. Уилкинс (1973). QUEST - Система доказательства неклаузальных теорем (магистерская диссертация). Univ. Эссекса, Англия.
- ^ а б Нил В. Мюррей (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (Технический отчет). Syracuse Univ. 2-79. (Цит. Из Manna, Waldinger, 1980 как: «Процедура доказательства для неклаузальной логики первого порядка», 1978)
- ^ а б в г Зохар Манна , Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ» . Транзакции ACM по языкам и системам программирования . 2 : 90–121. DOI : 10.1145 / 357084.357090 .Препринт появился в декабре 1978 г. как SRI Technical Note 177.
- ^ Н.В. Мюррей (1982). «Полностью неклаузальное доказательство теоремы». Искусственный интеллект . 18 : 67–85. DOI : 10.1016 / 0004-3702 (82) 90011-X .
- ^ а б в г д е Дж. Трауготт (1986). «Вложенное разрешение». Proc. 8-я конференция по автоматическому отчислению . LNCS . 230 . Springer. С. 394–403.
- ^ а б Шмерл, УР (1988). «Резолюция на деревьях формул». Acta Informatica . 25 : 425–438. DOI : 10.1007 / bf02737109 . Резюме
- ^ Эти понятия, называемые "полярностями", относятся к числу явных или неявных отрицаний, обнаруженных выше.. Например, происходит положительно в И в , отрицательный в И в , и в обеих полярностях в .
- ^ ""используется для обозначения упрощения после разрешения.
- ^ Здесь ""означает синтаксический термин равенство по модулю переименования
- ^ Nieuwenhuis, Роберт; Рубио, Альберто. «Доказательство теорем на основе параметризации». Справочник по автоматизированному мышлению (PDF) .
Рекомендации
- Робинсон , Дж. Алан (1965). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23–41. DOI : 10.1145 / 321250.321253 .
- Лейтч, Александр (1997). Исчисление разрешающей способности . Springer .
- Галлье, Жан Х. (1986). Логика для компьютерных наук: основы автоматического доказательства теорем . Издательство Harper & Row .
- Ли, Чин-Лян Чанг, Ричард Чар-Тунг (1987). Символическая логика и механическое доказательство теорем ([переиздание] ред.). Сан-Диего: Academic Press. ISBN 0-12-170350-9.
Внешние ссылки
- Алексей Сахаров. «Принцип разрешающей способности» . MathWorld .
- Алексей Сахаров. «Разрешение» . MathWorld .