Автор Тема: Сколемовская нормальная форма формулы логики предикатов  (Прочитано 3571 раз)

0 Пользователей и 2 Гостей просматривают эту тему.

Оффлайн Дмитрий

  • Пользователь
  • Сообщений: 10
    • Просмотр профиля
Найти сколемовскую нормальную форму формулы исчисления предикатов: \(  \large \exists x \ \forall y \ \exists z \ \exists t \ ( \neg (P(y) \vee Q(t)) R(x) S(z))  \).




 

Оффлайн Admin

  • Администратор
  • Сообщений: 4966
  • Поблагодарили: 1575 раз(а)
    • Просмотр профиля
Нормальная форма Сколема характеризуется кванторной приставкой вида \(  \large \forall x_1 \ \ldots \ \forall x_n \). Кроме того, бескванторная часть формулы должна быть представлена в конъюнктивной нормальной форме. Используя один из законов де Моргана, бескванторную часть рассматриваемой формулы можно представить в виде \(  \large \neg P(y) \cdot \neg Q(t) \cdot R(x) \cdot S(z) \). В кванторной приставке рассматриваемой формулы сначала идёт квантор существования, который связывает единственную предметную переменную предикатной переменной \(  \large R(x) \). Поэтому указанную предметную переменную следует заменить на некую константу \(  \large a \), а соответствующий квантор исключить. Имеем:

\(  \large \forall y \ \exists z \ \exists t ( \neg P(y) \cdot \neg Q(t) \cdot R(a) \cdot S(z)) \).

Рассмотрим кванторную приставку полученной формулы. Здесь квантору существования по переменной \(  \large z \) предшествует квантор общности, связывающий переменную \(  \large y \). Следовательно, переменную, связанную квантором существования нужно заменить на некоторую функцию \(  \large f \) от переменной, связанной квантором общности, а квантор существования вычеркнуть. Получим:

\(  \large \forall y \  \exists t ( \neg P(y) \cdot \neg Q(t) \cdot R(a) \cdot S(f(y))) \).

Аналогично. Левее квантора существования, связывающего переменную \(  \large t \), стоит квантор общности, который связывает переменную \(  \large y \). Заменяя переменную \(  \large t \) на функцию \(  \large g \) от переменной, которая связана квантором общности, и исключая квантор существования, получим сколемовскую нормальную форму формулы исчисления предикатов:

\(  \large \forall y \  ( \neg P(y) \cdot \neg Q(g(y)) \cdot R(a) \cdot S(f(y))) \).
 

Оффлайн kenguru

  • Пользователь
  • Сообщений: 46
  • Поблагодарили: 1 раз(а)
    • Просмотр профиля
Помогите привести формулу логики предикатов \(  \large (\forall x)(\exists y) (\forall z)(\exists u) (R(x,y,z,u)) \) к сколемовской нормальной форме.
 

Оффлайн Admin

  • Администратор
  • Сообщений: 4966
  • Поблагодарили: 1575 раз(а)
    • Просмотр профиля
Дана замкнутая формула логики предикатов \(  \large (\forall x)(\exists y) (\forall z)(\exists u) (R(x,y,z,u)) \). Рассмотрим кванторную приставку этой формулы. Перед квантором существования, связывающим переменную \(  \large y \), стоит квантор общности, связывающий переменную \(  \large x \). Следовательно, в предикатной переменной \(  \large R(x,y,z,u) \) заменим переменную \(  \large y \) на сколемовскую функцию \(  \large f \) от переменной \(  \large x \), а квантор существования по переменной \(  \large y \) элиминируем. Имеем:

\(  \large (\forall x)(\forall z)(\exists u) (R(x, f(x), z, u)) \).

Рассмотрим кванторную приставку полученной формулы логики предикатов. Перед квантором существования по переменной \(  \large u \) стоят кванторы общности по переменным \(  \large x \) и \(  \large z \). Значит, в предикатной переменной \(  \large R(x, f(x), z, u) \) заменим переменную \(  \large u \) на сколемовскую функцию \(  \large g \) от переменных \(  \large x \) и \(  \large z \), а квантор существования, связывающий переменную \(  \large u \), элиминируем. Получим:

\(  \large (\forall x)(\forall z) (R(x, f(x), z, g(x,z))) \).

Итак, формула

\(  \large (\forall x)(\forall z) (R(x, f(x), z, g(x,z))) \)

является сколемовской нормальной формой формулы

\(  \large (\forall x)(\exists y) (\forall z)(\exists u) (R(x,y,z,u)) \).
 
Сказали спасибо: kenguru

Оффлайн kenguru

  • Пользователь
  • Сообщений: 46
  • Поблагодарили: 1 раз(а)
    • Просмотр профиля
Сколемизация формулы логики предикатов
« Ответ #4 : Март 14, 2016, 02:05:31 pm »
Помогите пожалуйста ещё с одной задачей.
Нужно выполнить сколемизацию формулы логики предикатов:

\(  \large (\forall x) (\exists y) (\exists z)((P(x) \to R(x,y)) \vee Q(x,z) \vee (\exists t) (S(y,z,t)))  \).

 

Оффлайн Admin

  • Администратор
  • Сообщений: 4966
  • Поблагодарили: 1575 раз(а)
    • Просмотр профиля
Сколемизация формулы логики предикатов
« Ответ #5 : Март 16, 2016, 01:16:28 pm »
Приведём формулу логики предикатов к предварённой нормальной форме, для чего выразим импликацию через дизъюнкцию и отрицание, навесим квантор существования по предметной переменной \(  \large t \), отсутствующей в предикатных переменных \(  \large P(x) \), \(  \large R(x,y) \) и \(  \large Q(x,z) \), а затем вынесем квантор существования за скобки, используя свойство дистрибутивности данного квантора относительно дизъюнкции. Имеем:

\(  \large (\forall x) (\exists y) (\exists z)((P(x) \to R(x,y)) \vee Q(x,z) \vee (\exists t) (S(y,z,t))) \simeq  \)

\(  \large  \simeq (\forall x) (\exists y) (\exists z) (\exists t) ( \overline{P(x)} \vee R(x,y) \vee Q(x,z) \vee S(y,z,t)) \).
.

Теперь переходим непосредственно к сколемизации. Поскольку перед квантором существования, связывающим предметную переменную \(  \large y \), стоит квантор всеобщности, связывающий предметную переменную \(  \large x \), то в рассматриваемой формуле логики предикатов следует заменить все вхождения переменной \(  \large y \) на сколемовскую функцию \(  \large f \) от переменной \(  \large x \), а квантор существования, который связывает переменную \(  \large y \), вычеркнуть. Получим:

\(  \large (\forall x)  (\exists z) (\exists t) ( \overline{P(x)} \vee R(x,f(x)) \vee Q(x,z) \vee S(f(x),z,t)) \).

Руководствуясь теми же соображениями, заменяем предметную переменную \(  \large z \) на функцию \(  \large g(x) \), а предметную переменную \(  \large t \) - на функцию \(  \large h(x) \). Кванторы существования при этом исключаем. Имеем:

\(  \large (\forall x)   ( \overline{P(x)} \vee R(x,f(x)) \vee Q(x,g(x)) \vee S(f(x),g(x),h(x))) \).
 
Сказали спасибо: kenguru

Оффлайн kenguru

  • Пользователь
  • Сообщений: 46
  • Поблагодарили: 1 раз(а)
    • Просмотр профиля
Re: Сколемизация формулы логики предикатов
« Ответ #6 : Март 16, 2016, 04:20:26 pm »
Просто огромное спасибо!!!
 
Сказали спасибо: Илья23

Оффлайн Admin

  • Администратор
  • Сообщений: 4966
  • Поблагодарили: 1575 раз(а)
    • Просмотр профиля
Re: Сколемизация формулы логики предикатов
« Ответ #7 : Март 16, 2016, 05:51:49 pm »
Пожалуйста.
 
Сказали спасибо: Илья23