Мат. логика. Логика предикатов.
Добавлено: 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)]$$](http://fx.ifz.ru/tex2.php?d=120&i=%24%24%5Cexists%7Bz%7D%5Cforall%7Bv%7D%5Cexists%7Bu%7D%5Cexists%7By%7D%5Cexists%7Bw%7D%5Cforall%7Bu%7D%5Cforall%7Bx%7D%5B%5Coverline%7BB%7D%28b%2Cz%2Cz%29%2AA%28b%2Cv%2CB%29%5Cvee%7B%7D%5Coverline%7BB%7D%28u%2Cu%2Cu%29%2A%5Coverline%7BA%7D%28y%2Cy%2Cz%29%5Cvee%7B%7DB%28w%2Cc%2Cw%29%2AA%28u%2Cu%2Cu%29%5Cvee%7B%7DB%28b%2Cu%2Cw%29%2AB%28x%2Cc%2Cz%29%5D%24%24 "$$\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 в нём нужно множество формул.
Вопрос: как из полученной ПНФ достать это множество формул?
1) Привести к ПНФ (прендексный нормальный вид).
2) Затем полученное множество формул унифицировать.
3) И последнее, построить резллютивный вывод
Первый пункт я выполнил. И вот, что вышло
Для выполнения второго пункта у меня есть алгоритм. Ho в нём нужно множество формул.
Вопрос: как из полученной ПНФ достать это множество формул?