Лекции . Технология построения интеллектуальных систем. Методы представления знаний Формальные языки и формальные системы (стр. 7 )

;

- множество функциональных символов на уровне i.

Пример.

Пусть дано - константы, - функциональный символ.

Объединение всех этих множеств называется универсумом Эрбрана:

(У Лорьера: ).

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

Теорема Эрбрана

Множество предложений невыполнимо тогда и только тогда, когда существует конечное множество подформул этого множества , невыполнимое на универсуме Эрбрана.

Теорема о резолюции

Пусть (1),
где - предложения; 12 удовлетворяет тем же условиям, что и . Тогда формула такова, что ( выводима из ).

Фактически это означает, что из выражения и выражения выводимо выражение . Это выражение называется резольвентой выражений и , а выражения  и   называются родительскими дизъюнктами. получается как бы вычеркиванием контрарных пар и соединением дизъюнкцией оставшихся литералов.

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

Но сначала рассмотрим примеры.

Пример 1

Пусть (2)
Надо доказать, что эта формула невыполнима. Для этого надо найти родительские формулы и резольвенты. Найдя контрарные пары, будем иметь: , что и доказывает противоречивость формулы.

Имеем:

резольвируем дизъюнкты и . Получаем (вычеркнули контрарную пару ) резольвируем . Резольвента: . дизъюнкт дает пустой дизъюнкт.

Таким образом, получили противоречие, то есть формула (2) невыполнима (или противоречива с точки зрения синтаксического вывода). Доказав невыполнимость исходной формулы, доказали выполнимость формулы (2)

, что означает , то есть доказали, что , то есть доказали выводимость из  . Из истинности следует невыполнение 13.

Пример 2

Докажем корректность правила modus ponens (правило отделения):

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

Докажем, что эта теорема доказуема в логике исчисления предикатов первого порядка. Преобразуем это выражение к дизъюнктивной нормальной форме14.

- проверяем ее невыполнимость:

Рассмотрим . Резольвента: .

дает нам пустой дизъюнкт.

Следовательно, формула  невыполнима. То есть формула  выводима, то есть является теоремой.

Этот алгоритм удобен для машинной реализации.

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

Для приведения формул к такому виду существуют специальные алгоритмы. Рассмотрим один из них.

Приведение формулы к хорновскому (Horn) виду

Имеется последовательность шагов:

- вынесение кванторов за скобки. 15 - формула выражения эквивалентности через импликацию. - импликация выражается через дизъюнкцию.

Кроме того, стоит задача минимизации кванторов16. Рассмотрим выражения и . В первом случае, по сути, есть некоторая функция от квантованной переменной . Введем функциональный символ : . Избавляясь от квантора , получаем: . Этот переход называется элиминацией квантора существования. А сама формула - сколемовской  нормальной формой. В случае, когда имеем квантор существования, его можно просто опустить.

Алгоритм приведения формулы к сколемовской нормальной форме

Предполагается, что рассматривается уже отрицание формулы.