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

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

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

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

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

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

Правило разрешения в пропозициональной логике — это единственное допустимое правило вывода, которое создает новое предложение, подразумеваемое двумя предложениями, содержащими дополнительные литералы. Литерал — это пропозициональная переменная или отрицание пропозициональной переменной. Два литерала называются дополнительными, если один является отрицанием другого (далее: $\lnot c$ считается дополнением к $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}}

,

где $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$ имеет хотя бы один «отрицательный» и «положительный» ^[14] возникновение в $F$ и $G$ , соответственно. Мюррей показал, что это правило является полным, если дополнить его соответствующими правилами логического преобразования. ^[10]^: 103

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

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

,

где показатели $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]^{: 398–400}

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

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

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

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

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

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

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

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

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

Реализации

См. также

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

Примечания

^ Дэвис, Мартин; Патнэм, Хилари (1960). «Вычислительная процедура для количественной теории» . Дж. АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376 . Здесь: с. 210, «III. Правило исключения атомных формул».
^ Робинсон 1965
^ Д. Е. Кнут, Искусство компьютерного программирования 4A : Комбинаторные алгоритмы , часть 1, с. 539
^ Перейти обратно: ^а ^б Лейтч 1997 , с. 11 «Перед применением самого метода вывода мы преобразуем формулы к бескванторной конъюнктивной нормальной форме».
^ Да, Генри П.; Гонсалес, Джон Л.; Рубио, Фердинанд М. (2005). Вычислительная логика . Paraninfo Editions, SA ISBN 9788497321822 .
^ Рассел, Стюарт Дж.; Норвиг, Питер (2009). Искусственный интеллект: современный подход (3-е изд.). Прентис Холл. п. 350. ИСБН 978-0-13-604259-4 .
^ Даффи, Дэвид А. (1991). Принципы автоматического доказательства теорем . Уайли. ISBN 978-0-471-92784-6 . См. стр. 77. Приведенный здесь пример немного изменен, чтобы продемонстрировать нетривиальную факторинговую замену. Для ясности этап факторинга (5) показан отдельно. На этапе (6) новая переменная $w'$ был введен для обеспечения унификации (5) и (6), необходимой для (7).
^ Уилкинс, Д. (1973). КВЕСТ: Неклаузальная система доказательства теорем (магистерская диссертация). Университет Эссекса.
^ Перейти обратно: ^а ^б Мюррей, Нил В. (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (технический отчет). Электротехника и информатика, Сиракузский университет. 39. (Цитируется по Манне, Вальдингеру, 1980 г. как: «Процедура доказательства неклаузальной логики первого порядка», 1978 г.)
^ Перейти обратно: ^а ^б ^с ^д Манна, Зоар ; Уолдингер, Ричард (январь 1980 г.). «Дедуктивный подход к синтезу программ» . Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090 . S2CID 14770735 .
^ Мюррей, Невада (1982). «Полностью неклаузальное доказательство теорем». Искусственный интеллект . 18 : 67–85. дои : 10.1016/0004-3702(82)90011-x .
^ Перейти обратно: ^а ^б ^с ^д ^и ^ж Трауготт, Дж. (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 .

Ссылки

Робинсон , Дж. Алан (1965). «Машинно-ориентированная логика, основанная на принципе разрешения» . Журнал АКМ . 12 (1): 23–41. дои : 10.1145/321250.321253 . S2CID 14389185 .
Лейч, Александр (1997). Расчет разрешения . Тексты по теоретической информатике. Серия EATCS. Спрингер . ISBN 978-3-642-60605-2 .
Галье, Жан Х. (1986). Логика в информатике: основы автоматического доказательства теорем . Харпер и Роу .
Ли, Чин-Лян Чанг, Ричард Чар-Тунг (1987). Символическая логика и механическое доказательство теорем . Академическая пресса. ISBN 0-12-170350-9 . {{cite book}}: CS1 maint: несколько имен: список авторов ( ссылка )

Внешние ссылки

Алексей Сахаров. «Принцип разрешения» . Математический мир .
Алексей Сахаров. "Разрешение" . Математический мир .

[1] Дэвис, Мартин; Патнэм, Хилари (1960). «Вычислительная процедура для количественной теории» . Дж. АКМ . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376 . Здесь: с. 210, «III. Правило исключения атомных формул».

[2] Робинсон 1965

[3] Д. Е. Кнут, Искусство компьютерного программирования 4A : Комбинаторные алгоритмы , часть 1, с. 539

[leitsch-4] Перейти обратно: ^а ^б Лейтч 1997 , с. 11 «Перед применением самого метода вывода мы преобразуем формулы к бескванторной конъюнктивной нормальной форме».

[5] Да, Генри П.; Гонсалес, Джон Л.; Рубио, Фердинанд М. (2005). Вычислительная логика . Paraninfo Editions, SA ISBN 9788497321822 .

[6] Рассел, Стюарт Дж.; Норвиг, Питер (2009). Искусственный интеллект: современный подход (3-е изд.). Прентис Холл. п. 350. ИСБН 978-0-13-604259-4 .

[7] Даффи, Дэвид А. (1991). Принципы автоматического доказательства теорем . Уайли. ISBN 978-0-471-92784-6 . См. стр. 77. Приведенный здесь пример немного изменен, чтобы продемонстрировать нетривиальную факторинговую замену. Для ясности этап факторинга (5) показан отдельно. На этапе (6) новая переменная $w'$ был введен для обеспечения унификации (5) и (6), необходимой для (7).

[8] Уилкинс, Д. (1973). КВЕСТ: Неклаузальная система доказательства теорем (магистерская диссертация). Университет Эссекса.

[Murray.1979-9] Перейти обратно: ^а ^б Мюррей, Нил В. (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (технический отчет). Электротехника и информатика, Сиракузский университет. 39. (Цитируется по Манне, Вальдингеру, 1980 г. как: «Процедура доказательства неклаузальной логики первого порядка», 1978 г.)

[Manna.Waldinger.1980-10] Перейти обратно: ^а ^б ^с ^д Манна, Зоар ; Уолдингер, Ричард (январь 1980 г.). «Дедуктивный подход к синтезу программ» . Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090 . S2CID 14770735 .

[11] Мюррей, Невада (1982). «Полностью неклаузальное доказательство теорем». Искусственный интеллект . 18 : 67–85. дои : 10.1016/0004-3702(82)90011-x .

[Traugott.1986-12] Перейти обратно: ^а ^б ^с ^д ^и ^ж Трауготт, Дж. (1986). «Вложенное разрешение» . 8-я Международная конференция по автоматизированному дедукции. КАД 1986 . ЛНКС . Том. 230. Спрингер. стр. 394–403. дои : 10.1007/3-540-16780-3_106 . ISBN 978-3-540-39861-5 .

[Schmerl.1988-13] Перейти обратно: ^а ^б Шмерл, UR (1988). «Решение о деревьях формул». Акта Информатика . 25 (4): 425–438. дои : 10.1007/bf02737109 . S2CID 32702782 . Краткое содержание

[14] Эти понятия, называемые «полярностями», относятся к количеству явных или неявных отрицаний, найденных выше. $p$ . Например, $p$ бывает положительным в $(p\land q)\lor r$ и в $q\rightarrow p$ , отрицательный в $\lnot (p\land q)\lor r$ и в $p\rightarrow q$ , и в обеих полярностях в $p\leftrightarrow q$ .

[15] " $\implies$ " используется для обозначения упрощения после разрешения.

[16] Здесь " $=$ «обозначает синтаксическое равенство терминов по модулю переименования

[Rubio-17] Ньювенхейс, Роберт; Рубио, Альберто (2001). «7. Доказательство теорем на основе парамодуляции» (PDF) . В Робинсоне, Алан Дж.А.; Воронков, Андрей (ред.). Справочник по автоматизированному рассуждению . Эльзевир. стр. 371–444. ISBN 978-0-08-053279-0 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]