Средства разработки приложений


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


Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:

  1. пользуясь эквивалентностью A → B ≡ ¬A ∨ B исключим импликацию;
  2. перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности: ¬(A ∨ B) ≡ ¬A ∧ ¬B ¬(A ∧ B) ≡ ¬A ∨ ¬B ¬(∃xA) ≡ ∀x¬A ¬(∀xA) ≡ ∃x¬A ¬¬A ≡ A
  3. переименовываем связанные переменные так, чтобы ни одна переменная не входила в нашу формулу одновременно связанно и свободно.
  4. выносим кванторы в начало формулы, используя эквивалентности:

    QxA(x) ∨ B ≡ Qx(A(x) ∨ B), если B не содержит переменной x, а Q ∈ {∀, ∃}

    QxA(x) ∧ B ≡ Qx(A(x) ∧ B), если B не содержит переменной x, а Q ∈ {∀, ∃}

    ∀xA(x) ∧ ∀xB(x) ≡ ∀x(A(x) ∧ B(x)) ∃xA(x) ∨ ∃xB(x) ≡ ∃x(A(x) ∨ B(x))

    Q1xA(x) ∨ Q2xB ≡ Q1xQ2y(A(x) ∨ B(y)), где Q ∈ {∀, ∃}

    Q1xA(x) ∧ Q2xB ≡ Q1xQ2y(A(x) ∧ B(y)), где Q ∈ {∀, ∃}

Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле кванторы существования. Для этого для каждого квантора существования выполним следующий алгоритм.

Если устраняемый квантор существования — самый левый квантор в префиксе формулы, заменим все вхождения в формулу переменной, связанной этим квантором, на новую константу и вычеркнем квантор из префикса формулы.

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

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм устранения кванторов существования придумал Сколем в 1927 году.

Имеет место теорема о том, что формула и ее сколемизация эквивалентны в смысле выполнимости.




Начало  Назад  Вперед



Книжный магазин