Разрешение (логика)

В математической логике и автоматизированном доказательстве теорем резолюция — это правило вывода, приводящее к методу доказательства теоремы , полной опровержения, для предложений в пропозициональной логике и логике первого порядка . Для пропозициональной логики систематическое применение правила резолюции действует как процедура принятия решения о невыполнимости формулы, решая (дополнение) к проблеме булевой выполнимости . Для логики первого порядка резолюция может быть использована в качестве основы для полуалгоритма для проблемы невыполнимости логики первого порядка , предоставляя более практичный метод, чем тот, который следует из теоремы Гёделя о полноте .

Правило разрешения можно проследить до Дэвиса и Патнэма (1960); ^[1] однако, их алгоритм требовал перебора всех основных экземпляров данной формулы. Этот источник комбинаторного взрыва был устранен в 1965 году синтаксическим алгоритмом унификации Джона Алана Робинсона , который позволял инстанцировать формулу во время доказательства «по требованию» ровно настолько, насколько это было необходимо для сохранения полноты опровержения . ^[2]

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

Правило разрешения в пропозициональной логике — это единственное допустимое правило вывода, которое создает новое предложение, подразумеваемое двумя предложениями, содержащими дополнительные литералы. Литерал — это пропозициональная переменная или отрицание пропозициональной переменной. Два литерала называются дополнениями, если один из них является отрицанием другого (в дальнейшем подразумевается дополнение к ). Результирующее предложение содержит все литералы, которые не имеют дополнений. Формально:${\displaystyle \lnot c}$${\displaystyle с}$

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

где

все , , и являются литералами,${\displaystyle a_{i}}$${\displaystyle b_{i}}$${\displaystyle c}$

разделительная линия означает « влечет за собой ».

Вышесказанное можно также записать так:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

Или схематически так:

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

У нас есть следующая терминология:

• Приложения и являются посылками вывода.${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$(разрешающая сила посылок) является их заключением.
• Литерал — это леворазрешенный литерал,${\displaystyle \ell }$
• Литерал — это правильно разрешённый литерал,${\displaystyle {\overline {\ell }}}$
• ${\displaystyle |\ell |}$это разрешенный атом или стержень.

Предложение, полученное по правилу резолюции, называется резольвентой двух входящих предложений. Это принцип консенсуса, применяемый к предложениям, а не к терминам. ^[3]

Если два предложения содержат более одной пары дополнительных литералов, правило разрешения может быть применено (независимо) для каждой такой пары; однако результатом всегда будет тавтология .

Modus ponens можно рассматривать как частный случай резолюции (однобуквенного предложения и двубуквенного предложения).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

эквивалентно

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

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

Этот метод разрешения использует доказательство от противного и основан на том факте, что любое предложение в пропозициональной логике может быть преобразовано в эквивалентное предложение в конъюнктивной нормальной форме . ^[4] Шаги следующие.

• Все предложения в базе знаний и отрицание предложения, которое необходимо доказать ( предположение ), связаны конъюнктивно.
• Полученное предложение преобразуется в конъюнктивную нормальную форму, где конъюнкты рассматриваются как элементы в наборе S предложений. ^[4]
  • Например, порождает множество .${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$
• Правило разрешения применяется ко всем возможным парам предложений, содержащих дополнительные литералы. После каждого применения правила разрешения результирующее предложение упрощается путем удаления повторяющихся литералов. Если предложение содержит дополнительные литералы, оно отбрасывается (как тавтология). Если нет, и если оно еще не присутствует в наборе предложений S , оно добавляется к S и рассматривается для дальнейших выводов разрешения.
• Если после применения правила разрешения выводится пустое предложение , то исходная формула невыполнима (или противоречива ), и, следовательно, можно сделать вывод, что исходная гипотеза следует из аксиом.
• Если, с другой стороны, пустое предложение не может быть выведено, и правило разрешения не может быть применено для вывода новых предложений, то гипотеза не является теоремой исходной базы знаний.

Одним из примеров этого алгоритма является оригинальный алгоритм Дэвиса–Патнэма , который впоследствии был усовершенствован до алгоритма DPLL , устранившего необходимость явного представления резольвент.

Это описание техники разрешения использует множество S в качестве базовой структуры данных для представления выводов разрешения. Списки , деревья и направленные ациклические графы являются другими возможными и распространенными альтернативами. Древовидные представления более верны тому факту, что правило разрешения является бинарным. Вместе с последовательной нотацией для предложений древовидное представление также позволяет ясно увидеть, как правило разрешения связано с особым случаем правила разреза , ограниченного атомарными формулами разреза. Однако древовидные представления не столь компактны, как представления множеств или списков, поскольку они явно показывают избыточные подвыводы предложений, которые используются более одного раза при выводе пустого предложения. Графовые представления могут быть столь же компактными по количеству предложений, как и списочные представления, и они также хранят структурную информацию относительно того, какие предложения были разрешены для вывода каждого резольвента.

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$

Проще говоря: Предположим , что ложно. Для того, чтобы посылка была истинной, должно быть истинным. Или же предположим, что истинно. Для того, чтобы посылка была истинной, должно быть истинным. Поэтому, независимо от ложности или истинности , если обе посылки верны, то заключение истинно.${\displaystyle a}$${\displaystyle a\vee b}$${\displaystyle b}$${\displaystyle a}$${\displaystyle \neg a\vee c}$${\displaystyle c}$${\displaystyle a}$${\displaystyle b\vee c}$

Правило разрешения можно обобщить до логики первого порядка : ^[5]

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

где — наиболее общий объединитель и , причем и не имеют общих переменных.${\displaystyle \phi }$${\displaystyle L_{1}}$${\displaystyle {\overline {L_{2}}}}$${\displaystyle \Gamma _{1}}$${\displaystyle \Gamma _{2}}$

В предложениях и это правило можно применять с объединителем.${\displaystyle P(x),Q(x)}$${\displaystyle \neg P(b)}$${\displaystyle [b/x]}$

Здесь x — переменная, а b — константа.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

Здесь мы видим, что

• Приложения и являются посылками вывода.${\displaystyle P(x),Q(x)}$${\displaystyle \neg P(b)}$
• ${\displaystyle Q(b)}$(разрешающая сила посылок) является их заключением.
• Литерал — это леворазрешенный литерал,${\displaystyle P(x)}$
• Литерал — это правильно разрешённый литерал,${\displaystyle \neg P(b)}$
• ${\displaystyle P}$это разрешенный атом или стержень.
• ${\displaystyle [b/x]}$является наиболее общим объединителем разрешенных литералов.

В логике первого порядка резолюция сводит традиционные силлогизмы логического вывода к одному правилу.

Чтобы понять, как работает разрешение, рассмотрим следующий пример силлогизма терминологической модели :

Все греки — европейцы.

Гомер — грек.

Следовательно, Гомер — европеец.

Или, в более общем смысле:

${\displaystyle \forall x.P(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

Поэтому,${\displaystyle Q(a)}$

Чтобы переформулировать рассуждение с использованием техники резолюции, сначала предложения должны быть преобразованы в конъюнктивную нормальную форму (CNF). В этой форме вся квантификация становится неявной: универсальные квантификаторы по переменным ( X , Y , ...) просто опускаются, как и предполагалось, в то время как экзистенциально-квантифицированные переменные заменяются функциями Сколема .

${\displaystyle \neg P(x)\vee Q(x)}$

${\displaystyle P(a)}$

Поэтому,${\displaystyle Q(a)}$

Итак, вопрос в том, как техника резолюции выводит последнее предложение из первых двух? Правило простое:

• Найдите два предложения, содержащие один и тот же предикат, где в одном предложении он отрицается, а в другом — нет.
• Выполните объединение двух предикатов. (Если объединение не удалось, вы сделали плохой выбор предикатов. Вернитесь к предыдущему шагу и попробуйте снова.)
• Если какие-либо несвязанные переменные, которые были связаны в объединенных предикатах, также встречаются в других предикатах в двух предложениях, замените их связанными значениями (терминами) и там.
• Отбросьте объединенные предикаты и объедините оставшиеся из двух предложений в новое предложение, также соединенное оператором «∨».

Чтобы применить это правило к приведенному выше примеру, мы обнаруживаем, что предикат P встречается в отрицательной форме.

¬ П ( Х )

в первом предложении и в неотрицательной форме

П ( а )

во втором предложении. X — это несвязанная переменная, а a — связанное значение (термин). Объединение двух приводит к замене

Х ↦ а

Отбрасывая объединенные предикаты и применяя эту замену к оставшимся предикатам (в данном случае просто Q ( X ), получаем вывод:

В ( а )

В качестве другого примера рассмотрим силлогистическую форму

Все критяне — островитяне.

Все островитяне — лжецы.

Следовательно, все критяне — лжецы.

Или, в более общем смысле,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

Следовательно, ∀ X P ( X ) → R ( X )

В CNF антецеденты становятся:

¬ П ( Х ) ∨ Q ( Х )

¬ Q ( Y ) ∨ R ( Y )

(Переменная во втором предложении была переименована, чтобы было ясно, что переменные в разных предложениях различны.)

Теперь, объединение Q ( X ) в первом предложении с ¬ Q ( Y ) во втором предложении означает, что X и Y в любом случае становятся одной и той же переменной. Подстановка этого в оставшиеся предложения и их объединение дает вывод:

¬ П ( Х ) ∨ Р ( Х )

Правило резолюции, как определено Робинсоном, также включало факторизацию, которая объединяет два литерала в одном и том же предложении, до или во время применения резолюции, как определено выше. Полученное правило вывода является опровержением-полным, ^[6] в том смысле, что набор предложений невыполним, если и только если существует вывод пустого предложения, использующего только разрешение, улучшенное факторизацией.

Примером набора невыполнимых положений, для которого требуется факторизация для получения пустого положения, является:

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f(w))\\(3):&\lnot P(x)&\lor &\lnot P(f(x))\\\end{array}}}$

Поскольку каждое предложение состоит из двух литералов, то же самое делает и каждое возможное резольвентное предложение. Поэтому, путем разрешения без факторизации, пустое предложение никогда не может быть получено. Используя факторизацию, его можно получить, например, следующим образом: ^[7]

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{by resolving (1) and (2), with }}v=f(u)\\(5):&P(f(w))&{\text{by factoring (4), with }}u=f(w)\\(6):&\lnot P(f(f(w')))&{\text{by resolving (5) and (3), with }}w=w',x=f(w')\\(7):&{\text{false}}&{\text{by resolving (5) and (6), with }}w=f(w')\\\end{array}}}$

Были разработаны обобщения вышеуказанного правила резолюции, которые не требуют, чтобы исходные формулы были в клаузальной нормальной форме . ^{[8] [9] [10] [11] [12] [13]}

Эти методы полезны в основном в интерактивном доказательстве теорем, где важно сохранить читаемость человеком промежуточных формул результатов. Кроме того, они позволяют избежать комбинаторного взрыва во время преобразования в форму предложения, ^{[10] : 98} и иногда экономят шаги разрешения. ^{[13] : 425}

Для пропозициональной логики Мюррей ^{[9] : 18} и Манна и Уолдингер ^{[10] : 98} используют правило

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit {true}}]\lor G[{\textit {false}}]\\\end{array}}}$,

где обозначает произвольную формулу, обозначает формулу, содержащую в качестве подформулы, и строится путем замены в каждом вхождении на ; аналогично для . Резольвента должна быть упрощена с использованием таких правил, как , и т. д. Чтобы предотвратить создание бесполезных тривиальных резольвент, правило должно применяться только тогда, когда имеет хотя бы одно «отрицательное» и «положительное» ^[14] вхождение в и , соответственно. Мюррей показал, что это правило является полным, если дополнено соответствующими правилами логического преобразования. ^{[10] : 103}${\displaystyle p}$${\displaystyle F[p]}$${\displaystyle p}$${\displaystyle F[{\textit {true}}]}$${\displaystyle F[p]}$${\displaystyle p}$${\displaystyle {\textit {true}}}$${\displaystyle G}$${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$${\displaystyle q\land {\textit {true}}\implies q}$${\displaystyle p}$${\displaystyle F}$${\displaystyle G}$

Трауготт использует правило

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{array}}}$,

где показатели степеней указывают полярность его вхождений. В то время как и строятся как и прежде, формула получается путем замены каждого положительного и каждого отрицательного вхождения в на и , соответственно. Подобно подходу Мюррея, к резольвенте должны быть применены соответствующие упрощающие преобразования. Трауготт доказал, что его правило является полным, при условии, что в формулах используются только связки. ^{[12] : 398–400}${\displaystyle p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$${\displaystyle p}$${\displaystyle F}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$

Резольвента Трауготта сильнее резольвенты Мюррея. ^{[12] : 395} Более того, она не вводит новые бинарные юнкторы, тем самым избегая тенденции к клаузальной форме в повторном разрешении. Однако формулы могут стать длиннее, когда малое заменяется несколько раз большим и/или . ^{[12] : 398}${\displaystyle p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$

В качестве примера, исходя из предположений, данных пользователем

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4):&\lnot (a&\rightarrow &e)\\\end{array}}}$

Правило Мюррея можно использовать следующим образом, чтобы вывести противоречие: ^[15]

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\implies &d\lor \lnot a&{\mbox{from (2) and (1), with }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\lor &({\textit {false}}\lor \lnot a)&\implies &(b\rightarrow e)\lor \lnot a&{\mbox{from (3) and (5), with }}p=d\\(7):&(({\textit {true}}\rightarrow e)\lor \lnot a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\lor \lnot a\lor \lnot a&{\mbox{from (6) and (1), with }}p=b\\(8):&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\implies &e&{\mbox{from (7) and (4), with }}p=a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) and (8), with }}p=e\\\end{array}}}$

Для этой же цели можно использовать правило Трауготта следующим образом: ^{[12] : 397}

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{from (1) and (2), with }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\implies &a\rightarrow e&{\mbox{from (10) and (3), with }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{from (11) and (4), with }}p=(a\rightarrow e)\\\end{array}}}$

При сравнении обоих вычетов можно выявить следующие проблемы:

• Правило Трауготта может дать более точную резольвенту: сравните (5) и (10), которые оба разрешают (1) и (2) относительно .${\displaystyle p=c}$
• Правило Мюррея ввело 3 новых символа дизъюнкции: в (5), (6) и (7), тогда как правило Трауготта не ввело ни одного нового символа; в этом смысле промежуточные формулы Трауготта больше напоминают стиль пользователя, чем Мюррея.
• Из-за последней проблемы правило Трауготта может воспользоваться импликацией в предположении (4), используя как неатомарную формулу в шаге (12). Используя правила Мюррея, семантически эквивалентная формула была получена как (7), однако, она не могла быть использована как из-за ее синтаксической формы.${\displaystyle p}$ ${\displaystyle a\rightarrow e}$${\displaystyle e\lor \lnot a\lor \lnot a}$${\displaystyle p}$

Для логики предикатов первого порядка правило Мюррея обобщается, чтобы разрешить различные, но унифицируемые подформулы и для и , соответственно. Если является наиболее общим унификатором для и , то обобщенная резольвента — . Хотя правило остается верным, если используется более специальная подстановка, для достижения полноты такие применения правил не требуются. ^{[ необходима цитата ]}${\displaystyle p_{1}}$${\displaystyle p_{2}}$${\displaystyle F}$${\displaystyle G}$${\displaystyle \phi }$${\displaystyle p_{1}}$${\displaystyle p_{2}}$${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]}$${\displaystyle \phi }$

Правило Трауготта обобщено, чтобы разрешить несколько попарно различных подформул и , при условии, что они имеют общий наиболее общий объединитель, скажем . Обобщенная резольвента получается после применения к родительским формулам, что делает пропозициональную версию применимой. Доказательство полноты Трауготта основано на предположении, что используется это полностью общее правило; ^{[12] : 401} неясно, останется ли его правило полным, если ограничиться и . ^[16]${\displaystyle p_{1},\ldots ,p_{m}}$${\displaystyle F}$${\displaystyle p_{m+1},\ldots ,p_{n}}$${\displaystyle G}$${\displaystyle p_{1},\ldots ,p_{n}}$${\displaystyle \phi }$${\displaystyle \phi }$${\displaystyle p_{1}=\cdots =p_{m}}$${\displaystyle p_{m+1}=\cdots =p_{n}}$

Парамодуляция — это родственная техника для рассуждений о множествах предложений, где предикатный символ — равенство. Она генерирует все «равные» версии предложений, за исключением рефлексивных тождеств. Операция парамодуляции берет положительное предложение from , которое должно содержать литерал равенства. Затем она ищет предложение into с подтермом, который унифицируется с одной стороной равенства. Затем подтерм заменяется другой стороной равенства. Общая цель парамодуляции — свести систему к атомам, уменьшив размер терминов при замене. ^[17]

• КАРИН
• ГКЦ
• Выдра
• Доказательство9
• СНАРК
• СПАСС
• Вампир
• Онлайн-доказательство Logictools

• Сжатый отряд  — более ранняя версия резолюции
• Индуктивное логическое программирование
• Обратное разрешение
• Логическое программирование
• Метод аналитических таблиц
• разрешение SLD
• Вывод о резолюции

• Робинсон , Дж. Алан (1965). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID  14389185.
• Leitsch, Alexander (1997). The Resolution Calculus. Тексты по теоретической информатике. Серия EATCS. ​​Springer . ISBN 978-3-642-60605-2.
• Галлье, Жан Х. (1986). Логика для компьютерных наук: основы автоматического доказательства теорем. Harper & Row .
• Ли, Чин-Лян Чан, Ричард Чар-Тунг (1987). Символическая логика и доказательство механических теорем . Academic Press. ISBN 0-12-170350-9.{{cite book}}: CS1 maint: multiple names: authors list (link)

• Алекс Сахаров. "Принцип разрешения". MathWorld .
• Алекс Сахаров. "Резолюция". MathWorld .