printЛогическое программирование

printЛогика предикатов. Метод резолюции

Исторически логика занимается изучением способов рассуждений, которые позволяли бы из истинных суждений-посылок всегда получать истинные суждения-заключения. Для современной логики характерно построение различного рода формализованных теорий логического рассуждения (логических исчислений), позволяющих сделать логические рассуждения предметом строгого анализа. Исчисление предикатов является одним из разделов математической логики и позволяет применять логические законы для изучения любой системы объектов с заданными для этих объектов свойствами и отношениями.
В логике предикатов используются следующие символы:
  • переменные: `x`,`y`,`z`,`u`,`v`,`w`,…;
  • константы, обозначающие конкретные объекты: `a`,`b`,`c`,`d`,`e`,…;
  • функциональные символы: `f`,`g`,`h`,…;
  • предикатные символы: `P`,`Q`,`R`,`S`,`T`,…;
  • логические символы: `∧`,`∨`,`⇒`,`¬`,`forall`,`EE`;
  • вспомогательные символы: ,().
Терм определяется индуктивно следующим образом.
  • Переменные и константы являются термами.
  • Если `f` – функция `m` аргументов, и `t_1,…,t_m` являются термами, то `f(t_1,…,t_m)` – терм.
Если `P` – предикатный символ `n` аргументов, `t_1,…,t_n` – термы, то `P(t_1,…,t_n)` называется атомарной формулой или атомом.
Логическая формула определяется с помощью следующих правил.
  • Атом – это логическая формула.
  • Если `A` и `B` – логические формулы, а `x` – переменная, то `(A)∨(B)`, `(A)∧(B)`, `(A)⇒(B)`, `¬(A)`, `forall\ x(A)`, `EE\ x(A)` являются логическими формулами.
Присвоив логическим символам соответствующие приоритеты, можно уменьшить число скобок.
Для получения из одних логических формул других существует много специальных правил вывода (modus ponens, modus tollens, дедуктивные правила и другие).
Систематизировать правила вывода начал Аристотель в «Первой аналитике». В дальнейшем к ним добавлялись новые формы и модусы расширялось и их количество достигло нескольких десятков. В средние века студенты даже учили стихи для запоминания основных 19 форм силлогизмов:
Barbara celarent darii ferio baralipton
Celantes dabitis fapesmo frisesomorum;
Cesare campestres festino baroco; darapti
Felapton disamis datisi bocardo ferison
Гласные в словах, взятые из латинских слов affirmo (я утверждаю) и nego (я отрицаю), указывали на качество и количество используемых для вывода утверждений:
a — общеутвердительные («Все люди смертны»)
i — частноутвердительные («Некоторые люди — студенты»)
e — общеотрицательные («Ни один из китов не рыба»)
o — частноотрицательные («Некоторые люди не являются студентами»)
Пример вывода для модуса Ferison:
Посылка 1: Ни одно дерево не съедобно.
Посылка 2: Некоторые деревья зелёные.
Заключение: Некоторые зелёные вещи не съедобны.
Для машинного вывода используется единственный способ вывода – принцип резолюции, – предложенный Дж.Робинсоном в 1965г.
Предположим имеются формулы `A_1,…,A_m` и `B`. Требуется доказать, что из формул `A_1,…,A_m` можно вывести формулу B. Доказательство основано на достоверности формулы `¬A_1∨…∨¬A_m∨B`, что следует из теоремы о полноте. Но проще доказать невыполнимость обратной формулы `A_1∧…∧A_m∧¬B`. Для этого формулу сначала приводят к сколемовской конъюнктивной нормальной форме. Процесс приведения состоит из следующих этапов.
1. Ограничение свободных переменных. Если `x_1,…,x_n` – свободные переменные, содержащиеся в `A`, то `A` преобразуется к виду `∃x_1\ …\ ∃x_n\ A`.
2. Переименование переменных, чтобы различные переменные имели разные имена.
3. Удаление символа `⇒`. `A⇒B` заменяется формулой `¬A∨B`.
4. Перемещение символа `¬` внутрь формул с символами `∨`, `∧`, `EE`, `forall`, пока `¬` не станет относиться к атомам. Для этого используются следующие правила замены:
`¬(A∧B)\ ->\ ¬A∨¬B`
`¬(A∨B)\ ->\ ¬A∧¬B`
`¬¬A\ ->\ A`
`¬∀x\ A\ ->\ ∃x\ ¬A`
`¬∃x\ A\ ->\ ∀x\ ¬A`
5. Удаление символа `EE`. Все переменные, связанные квантором `EE`, заменяются сколемовскими константами или функциями. Если переменная введена вне области действия квантора `forall`, то она заменяется константой. В противном случае переменная заменяется функцией от значений введенных квантором `forall` переменных, в области действия которых она была введена. Например,
`∃x∀y∀z∃u\ P(x,y,z,u)\ ->\ ∀y∀z\ P(a,y,z,f(y,z))`
6. Перемещение символов `forall` вперед и отбрасывание `forall`. Все свободные переменные считаются введенными квантором `forall`.
7. Перемещение символа `∨` относительно `∧`. Используется правило
`(A∧B)∨C\ ->\ (A∨C)∧(B∨C)`
8. Разделение формулы на набор дизъюнктов (предложений).
9. Минимизация. Атом с `¬` или без `¬` называется литералом. Удаляются повторяющиеся литералы. Удаляются предложения, литералы которых взаимно отрицают друг друга.
Иногда предложения представляют в форме клаузы (clause), записывая положительные литералы слева от знака стрелки, а отрицательные – справа. Например, предложение `A_1∨…∨A_m∨¬B_1∨…∨¬B_n` соответствует клаузе `A_1,…,A_m\ ->\ B_1,…,B_n`. Дизъюнкты, содержащие не более одного положительного литерала, называются хорновскими. Предложение с `m=1` и `n=0` соответствует факту в Прологе. Предложение с `m=1` и `n≥1` соответствует правилу в Прологе. Предложение с `m=0` и `n≥1` соответствует запросу в Прологе. Таким образом, Пролог представляет собой систему доказательства теорем методом резолюций для хорновских дизъюнктов. В принципе любая задача, выражаемая средствами логики, может быть выражена при помощи хорновских предложений.
Метод резолюции состоит в следующем. Пусть имеется два предложения `C_1=A_1∨…∨A_m∨D` и `C_2=B_1∨…∨B_n∨¬D`, содержащих один и тот же атом `D`. Резольвентой предложений `C_1` и `С_2` является предложение `С=A_1∨…∨A_m∨B_1∨…∨B_n`. Если литералы `D` и `¬D'` не равны, но существует унификатор, делающий их равными, то наиболее общий унификатор для `D` и `¬D'` применяется к предложениям `C_1` и `С_2`, а затем вычисляется их резольвента. Если резольвента `C` пуста, то это указывает на невыполнимость исходной формулы.
В случае нехорновских дизъюнктов метод резолюции необходимо дополнить правилом факторизации, применяемым для устранения повторяющихся литералов в одном предложении. Если литералы не равны, то также выполняется их унификация.
Рассмотрим простой пример. Пусть брадобреи бреют всех людей, которые не бреются сами и не бреют тех, кто бреется сам. Тогда брадобреи не существуют.
`A_1`: `∀x\ "Бб"(x)⇒∀y(¬Б(y,y)⇒Б(x,y))`
`A_2`: `∀x\ "Бб"(x)⇒∀y(Б(y,y)⇒¬Б(x,y))`
`B`: `¬∃x\ "Бб"(x)`
После перевода в сколемовскую конъюнктивную нормальную форму получаем предложения:
`C_1`: `¬"Бб"(x)∨Б(y,y)∨Б(x,y)`
`C_2`: `¬"Бб"(x)∨¬Б(y,y)∨¬Б(x,y)`
`C_3`: `"Бб"(a)`
Применяя метод резолюции и правило факторизации, получаем предложения:
`C_4`: `¬"Бб"(x)∨Б(x,x)` факторизация `C_1`
`C_5`: `¬"Бб"(x)∨¬Б(x,x)` факторизация `C_2`
`C_6`: `Б(a,a)` резольвента `C_3` и `C_4`
`C_7`: `¬Б(a,a)`резольвента `C_3` и `C_5`
`С_8`: `⊥`резольвента `C_6` и `C_7`
Рассмотрим еще один пример.
Каждого, кто любит всех животных, кто-то любит. Любого, кто убивает животных, никто не любит. Джек любит всех животных. Кота по имени Тунец убил либо Джек, либо Любопытство. Действительно ли этого кота убило Любопытство?
`A_1`: `∀x\ (∀y\ "Животное"(y)\ ⇒\ "Любит"(x,y))\ ⇒\ (∃z\ "Любит"(z,x))`
`A_2`: `∀x\ (∃y\ "Животное"(y)∧"Убил"(x,y))\ ⇒\ (∀z\ ¬"Любит"(z,x))`
`A_3`: `∀y\ "Животное"(y)\ ⇒\ "Любит"("Джек",y)`
`A_4`: `"Кот"("Тунец")\ ∧\ ("Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец"))`
`A_5`: `∀x\ "Кот"(x)\ ⇒\ "Животное"(x)`
`B`: `"Убил"("Любопытство","Тунец")`
Доказываем невыполнимость формулы:
`(∀x\ (∀y\ "Животное"(y)\ ⇒\ "Любит"(x,y))\ ⇒\ (∃z\ "Любит"(z,x)))`
`\ ∧\ (∀x\ (∃y\ "Животное"(y)∧"Убил"(x,y))\ ⇒\ (∀z\ ¬"Любит"(z,x)))`
`\ ∧\ (∀y\ "Животное"(y)\ ⇒\ "Любит"("Джек",y))`
`\ ∧\ ("Кот"("Тунец")\ ∧\ ("Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец")))`
`\ ∧\ (∀x\ "Кот"(x)\ ⇒\ "Животное"(x))`
`\ ∧\ ¬"Убил"("Любопытство","Тунец")`
После 3-го шага алгоритма получим:
`(∀x_1\ ¬(∀y_1\ ¬"Животное"(y_1)\ ∨\ "Любит"(x_1,y_1))\ ∨\ (∃z_1\ "Любит"(z_1,x_1)))`
`\ ∧\ (∀x_2\ ¬(∃y_2\ "Животное"(y_2)∧"Убил"(x_2,y_2))\ ∨\ (∀z_2\ ¬"Любит"(z_2,x_2)))`
`\ ∧\ (∀y_3\ ¬"Животное"(y_3)\ ∨\ "Любит"("Джек",y_3))`
`\ ∧\ ("Кот"("Тунец")\ ∧\ ("Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец")))`
`\ ∧\ (∀x_4\ ¬"Кот"(x_4)\ ∨\ "Животное"(x_4))`
`\ ∧\ ¬"Убил"("Любопытство","Тунец")`
После 4-го шага алгоритма получим:
`(∀x_1\ (∃y_1\ "Животное"(y_1)\ ∧\ ¬"Любит"(x_1,y_1))\ ∨\ (∃z_1\ "Любит"(z_1,x_1)))`
`\ ∧\ (∀x_2\ (∀y_2\ ¬"Животное"(y_2)∨¬"Убил"(x_2,y_2))\ ∨\ (∀z_2\ ¬"Любит"(z_2,x_2)))`
`\ ∧\ (∀y_3\ ¬"Животное"(y_3)\ ∨\ "Любит"("Джек",y_3))`
`\ ∧\ ("Кот"("Тунец")\ ∧\ ("Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец")))`
`\ ∧\ (∀x_4\ ¬"Кот"(x_4)\ ∨\ "Животное"(x_4))`
`\ ∧\ ¬"Убил"("Любопытство","Тунец")`
После 6-го шага алгоритма получим:
`(("Животное"(f(x_1))\ ∧\ ¬"Любит"(x_1,f(x_1)))\ ∨\ "Любит"(g(x_1),x_1))`
`\ ∧\ (¬"Животное"(y_2)\ ∨\ ¬"Убил"(x_2,y_2)\ ∨\ ¬"Любит"(z_2,x_2))`
`\ ∧\ (¬"Животное"(y_3)\ ∨\ "Любит"("Джек",y_3))`
`\ ∧\ "Кот"("Тунец")\ ∧\ ("Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец"))`
`\ ∧\ (¬"Кот"(x_4)\ ∨\ "Животное"(x_4))`
`\ ∧\ ¬"Убил"("Любопытство","Тунец")`
После завершения перевода в сколемовскую конъюнктивную нормальную форму получаем предложения:
`C_1`: `"Животное"(f(x))\ ∨\ "Любит"(g(x),x)`
`C_2`: `¬"Любит"(x,f(x))\ ∨\ "Любит"(g(x),x)`
`C_3`: `¬"Животное"(y)\ ∨\ ¬"Убил"(x,y)\ ∨\ ¬"Любит"(z,x)`
`C_4`: `¬"Животное"(y)\ ∨\ "Любит"("Джек",y)`
`C_5`: `"Кот"("Тунец")`
`C_6`: `"Убил"("Джек","Тунец")\ ∨\ "Убил"("Любопытство","Тунец")`
`C_7`: `¬"Кот"(x)\ ∨\ "Животное"(x)`
`C_8`: `¬"Убил"("Любопытство","Тунец")`
Применяя метод резолюции и правило факторизации, получаем предложения:
`C_9`: `"Животное"("Тунец")`резольвента `C_5` и `C_7`
`C_10`: `¬"Убил"(x,"Тунец")\ ∨\ ¬"Любит"(z,x)` резольвента `C_3` и `C_9`
`C_11`: `"Убил"("Джек","Тунец")` резольвента `C_6` и `C_8`
`C_12`: `¬"Любит"(z,"Джек")`резольвента `C_10` и `C_11`
`C_13`: `¬"Животное"(f("Джек"))\ ∨\ "Любит"(g("Джек"),"Джек")`резольвента `C_2` и `C_4`
`C_14`: `"Любит"(g("Джек"),"Джек")`резольвента `C_1` и `C_13` и факторизация
`С_15`: `⊥`резольвента `C_12` и `C_14`
Выбор посылок для применения резолюция является наиболее сложной проблемой, так как в нетривиальных случаях число предложений достаточно велико, а каждая новая резольвента увеличивает число кандидатов для применения резолюции.
loading