2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

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

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

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



Начать новую тему Ответить на тему
 
 Преобразование логической формулы
Сообщение20.04.2013, 13:50 


22/11/09
16
Здравствуйте.

Помогите, пожалуйста, разобраться.

Имеется следующее задание:
Преобразовать формулу, данную ниже, в форму, которая пригодна для процедур вывода.
Использовать правило Modus Ponens.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$

Ход решения.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$

Дадим всем переменным при кванторах уникальные имена.

$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists z W(z,x))$

Перенесем все кванторы в одну сторону.

$\forall x \forall y \exists z(P(y) \Rightarrow U(x,y)) \Rightarrow (W(z,x))$

Квантор существования заменим уникальной сколемовской функцией.

$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Опустим кванторы общности.

$(P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$

Выполним преобразования.

$(\neg P(y) \vee U(x,y)) \Rightarrow W(F(z),x)$

$\neg (\neg P(y) \vee U(x,y)) \vee W(F(z),x)$

$P(y) \wedge \neg U(x,y) \vee W(F(z),x)$

$\neg U(x,y) \wedge P(y) \vee W(F(z),x)$

Я сделал данные преобразования. И теперь вопросы.

  1. Мне не ясно что значит "форма пригодная для процедур вывода"? Это форма Хорна или что?
  2. Что значит использовать правило Modus Ponens в данном контексте?
  3. Верное ли решение?

Заранее спасибо.

 Профиль  
                  
 
 Re: Преобразование логической формулы
Сообщение20.04.2013, 14:00 
Заслуженный участник


08/04/08
8556
magneton_bora в сообщении #713131 писал(а):
$\forall x \forall y \exists z(P(y) \Rightarrow U(x,y)) \Rightarrow (W(z,x))$

Квантор существования заменим уникальной сколемовской функцией.

$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$
Надо писать не $F(z)$, а $F(x)$.
В остальном вроде верно.

magneton_bora в сообщении #713131 писал(а):
Мне не ясно что значит "форма пригодная для процедур вывода"? Это форма Хорна или что?
Это должно быть определено там, откуда Вы задачу взяли. Если форма, пригодная для процедур вывода, - это сколемовская нормальная форма, то все хорошо, иначе - нет.

magneton_bora в сообщении #713131 писал(а):
Что значит использовать правило Modus Ponens в данном контексте?
:shock: :? Может быть задание неполно?

 Профиль  
                  
 
 Re: Преобразование логической формулы
Сообщение20.04.2013, 14:14 


22/11/09
16
Цитата:
Надо писать не $F(z)$, а $F(x)$.
Хорошо, а почему?
Цитата:
Может быть задание неполно?
Исходное задание звучит следующим образом.
Transform the formula, given below, into a form that is appropriate for inference procedures applying the Modus Ponens inference rule.
Вот и пишу, потому что не могу понять что тут имеется в виду под "applying the Modus Ponens inference rule".

 Профиль  
                  
 
 Re: Преобразование логической формулы
Сообщение20.04.2013, 14:22 
Заслуженный участник


08/04/08
8556
magneton_bora в сообщении #713144 писал(а):
Хорошо, а почему?
Ну хотя бы так. Вы эквивалентно преобразуете замкнутую формулу
magneton_bora в сообщении #713131 писал(а):
$\forall x(\forall y P(y) \Rightarrow U(x,y)) \Rightarrow (\exists y W(y,x))$
в формулу со свободной переменной $z$
magneton_bora в сообщении #713131 писал(а):
$\forall x \forall y (P(y) \Rightarrow U(x,y)) \Rightarrow W(F(z),x)$
Некорректно же. Посмотрите процедуру сколемизации, если хочется смысл понять - возьмите конкретный пример (например, для любого эпсилон, существует эн зависящее от эпсилон... - двух кванторов и одного предиката хватит)

magneton_bora в сообщении #713144 писал(а):
Transform the formula, given below, into a form that is appropriate for inference procedures applying the Modus Ponens inference rule.
Вот я Inglish плохо знаю, но понял так: привести формулу к форме, пригодную к процедуре вывода, использующей [только] Modus Ponens (т.е. правил вывода с кванторами нету). Отсюда действительно следует, что нам надо избавиться от кванторов. Если сомневаетесь, можете уточнить здесь: topic10065-375.html

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 4 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group