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

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

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

Предложение, созданное правилом разрешения, иногда называют резольвентой .

Разрешение в пропозициональной логике

Правило разрешения

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

{\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 }}

где

все , , и являются литералами,

a_{i}

b_{i}

c

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

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

{\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 )}}

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

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

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

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

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

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

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

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

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

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

Техника разрешения

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

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

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

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

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

Простой пример

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

Говоря простым языком: «Предположение» неверно. Для того чтобы посылка была истинной, она должна быть истинной. Альтернативно, предположим, что это правда. Для того чтобы посылка была истинной, она должна быть истинной. Следовательно, независимо от ложности или правдивости утверждения , если обе посылки верны, то вывод истинен. $a$ $a\vee b$ $b$ $a$ $\neg a\vee c$ $c$ $a$ $b\vee c$

Разрешение в логике первого порядка

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

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

где является наиболее общим унификатором и , и и не имеют общих переменных . $\phi$ $L_{1}$ ${\overline {L_{2}}}$ $\Gamma _{1}$ $\Gamma _{2}$

Пример

Предложения и могут применять это правило в качестве унификатора. $P(x),Q(x)$ $\neg P(b)$ $[b/x]$

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

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

Здесь мы видим это

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

Неофициальное объяснение

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

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

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

Гомер — грек.

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

Или, в более общем плане:

\forall x.P(x)\Rightarrow Q(x)

P(a)

Поэтому,

Q(a)

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

\neg P(x)\vee Q(x)

P(a)

Поэтому,

Q(a)

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

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

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

¬ П ( Икс )

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

П ( а )

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

Икс ↦ а

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

Вопрос ( а )

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

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

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

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

Или, в более общем плане,

∀ Икс п ( Икс ) → Q ( Икс )

∀ Икс Q ( Икс ) → р ( Икс )

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

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

¬ п ( Икс ) ∨ Q ( Икс )

¬ Q ( Y ) ∨ р ( Y )

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

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

¬ п ( Икс ) ∨ р ( Икс )

Факторинг

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

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

{\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]

{\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} используют правило

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

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

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

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

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

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

Пример пропозиционального неклаузального разрешения

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

{\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]

{\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}

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

Неклаузальное разрешение в логике первого порядка

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

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

Парамодуляция

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

Реализации

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

Смотрите также

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

Примечания

^ Дэвис, Мартин; Патнэм, Хилари (1960). «Вычислительная процедура для количественной теории». Дж. АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376.Здесь: с. 210, «III. Правило исключения атомных формул».
^ Робинсон 1965
^ Д. Е. Кнут, Искусство компьютерного программирования 4A : Комбинаторные алгоритмы , часть 1, с. 539
^ ab Leitsch 1997, с. 11 «Перед применением самого метода вывода мы преобразуем формулы к бескванторной конъюнктивной нормальной форме».
^ Арис, Энрике П.; Гонсалес, Хуан Л.; Рубио, Фернандо М. (2005). Вычислительная логика. Ediciones Paraninfo, SA ISBN 9788497321822.
^ Рассел, Стюарт Дж.; Норвиг, Питер (2009). Искусственный интеллект: современный подход (3-е изд.). Прентис Холл. п. 350. ИСБН 978-0-13-604259-4.
^ Даффи, Дэвид А. (1991). Принципы автоматического доказательства теорем . Уайли. ISBN 978-0-471-92784-6.См. стр. 77. Приведенный здесь пример немного изменен, чтобы продемонстрировать нетривиальную факторинговую замену. Для ясности этап факторинга (5) показан отдельно. На этапе (6) была введена новая переменная , чтобы обеспечить унификацию (5) и (6), необходимую для (7). $w'$
^ Уилкинс, Д. (1973). КВЕСТ: Неклаузальная система доказательства теорем (магистерская диссертация). Университет Эссекса.
^ аб Мюррей, Нил В. (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (технический отчет). Электротехника и информатика, Сиракузский университет. 39.(Цитируется по Манне, Вальдингеру, 1980 г. как: «Процедура доказательства неклаузальной логики первого порядка», 1978 г.)
^ abcd Манна, Зоар ; Уолдингер, Ричард (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090. S2CID 14770735.
^ Мюррей, Невада (1982). «Полностью неклаузальное доказательство теорем». Искусственный интеллект . 18 : 67–85. дои : 10.1016/0004-3702(82)90011-x.
^ abcdef Трауготт, Дж. (1986). «Вложенное разрешение». 8-я Международная конференция по автоматизированному дедукции. КАД 1986 . ЛНКС . Том. 230. Спрингер. стр. 394–403. дои : 10.1007/3-540-16780-3_106. ISBN 978-3-540-39861-5.
^ аб Шмерл, UR (1988). «Решение о деревьях формул». Акта Информатика . 25 (4): 425–438. дои : 10.1007/bf02737109. S2CID 32702782.Краткое содержание
^ Эти понятия, называемые «полярностями», относятся к количеству явных или неявных отрицаний, найденных выше . Например, встречается положительное значение в и в , отрицательное в и в , а также в обеих полярностях в . $p$ $p$ $(p\land q)\lor r$ $q\rightarrow p$ $\lnot (p\land q)\lor r$ $p\rightarrow q$ $p\leftrightarrow q$
^ " " используется для обозначения упрощения после разрешения. $\implies$
^ Здесь « » обозначает синтаксическое равенство терминов по модулю переименования. $=$
^ Ньювенхейс, Роберт; Рубио, Альберто (2001). «7. Доказательство теорем на основе парамодуляции» (PDF) . В Робинсоне, Алан Дж.А.; Воронков, Андрей (ред.). Справочник по автоматизированному рассуждению. Эльзевир. стр. 371–444. ISBN 978-0-08-053279-0.