Мат. логика. Логика предикатов.

mrMoRiC · Сообщение **mrMoRiC** » 07 июн 2009, 05:50

Здравствуйте. Преподаватель дал решить пример (формулу) повышенной сложности. И сказал сделать c ней следующее:

1) Привести к ПНФ (прендексный нормальный вид).
2) Затем полученное множество формул унифицировать.
3) И последнее, построить резллютивный вывод

Первый пункт я выполнил. И вот, что вышло
$\exists{z}\forall{v}\exists{u}\exists{y}\exists{w}\forall{u}\forall{x}[\overline{B}(b,z,z)*A(b,v,B)\vee{}\overline{B}(u,u,u)*\overline{A}(y,y,z)\vee{}B(w,c,w)*A(u,u,u)\vee{}B(b,u,w)*B(x,c,z)]$

Для выполнения второго пункта у меня есть алгоритм. Ho в нём нужно множество формул.

Вопрос: как из полученной ПНФ достать это множество формул?

mrMoRiC · Сообщение **mrMoRiC** » 08 июн 2009, 01:09

Есть подозрение, что нужно отбросить приставку полученной ПНФ, т.e. убрать эту часть

$\exists{z}\forall{v}\exists{u}\exists{y}\exists{w}\forall{u}\forall{x}$

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

Ho я не уверен в правильности моих рассуждений. Кто-нибудь из профи напишите своё мнение пожалуйста.

yourdomain.com