Главная страница
Навигация по странице:

  • Сколемовская и клаузальная формы.

  • Сколемовская и клаузальная формы

  • Лекция 6. Сколемовская стандартная форма, предварённая стандартная форма


    Скачать 37 Kb.
    НазваниеСколемовская стандартная форма, предварённая стандартная форма
    АнкорЛекция 6.doc
    Дата14.01.2018
    Размер37 Kb.
    Формат файлаdoc
    Имя файлаЛекция 6.doc
    ТипЛекция
    #3467





    Лекция №6

    Тема: Сколемовская стандартная форма, предварённая стандартная форма.

    План:

    1. Предварённая стандартная форма.

    2. Сколемовская и клаузальная формы.




    1. Предварённая стандартная форма.

    В логике высказываний были введены две нормальные формы: конъюнктивная и дизъюнктивная. Приведение формулы логики высказываний к одной из этих форм позволяет упростить алгоритмы доказательства выполнимости и общезначимости. По аналогичным причинам вводится нормальная форма и в исчислении предикатов.

    Определение. Предварённой формой называется формула, состоящая из высказываний, перед которыми стоит префикс, т.е. некоторая конечная последовательность квантификаций. Внутри высказываний кванторов нет.

    Таким образом, предваренная формула имеет вид:

    K1K2…Kn A,

    где Кi – обозначает либо , либо , для i = 1,…n и А – формула, не содержащая квантификаций.

    Теорема. для любой логической формулы существует логически эквивалентная ей предварённая нормальная форма.

    Этапы получения предварённой формы.

    Исключить связки эквивалентности и импликации.

    Переименовать (если необходимо) связанные переменные таким образом, чтобы никакая переменная не имела бы одновременно свободных и связанных вхождений.
    xA(x)  tA(t) x, t M.

    Удалить те квантификации, область действия которых не содержит вхождений квантифицированной переменной.

    Преобразовать все вхождения отрицания, состоящие непосредственно перед атомами.

    Переместить все квантификации в начало формулы. Для этого используется правила:

    (x A & xB) x(A & B),

    (x A(x) & B) x(A(x) & B), если В не содержит x,

    (A & x B(x) ) x(A & B(x)), если A не содержит x,

    (x A(x) & B)  x(A(x) & B), если В не содержит x,

    (A & x B(x))  x(A& B(x)), если A не содержит x.

    Замечание. одна формула может допускать много эквивалентных предварённых форм. Вид результата зависит от порядка применения правил, а также от произвола при переименовании переменных.

    Пример. Найдём предварённую нормальную форму для формулы:

    x[P(x) & yx( Q(x, y) ® z R(a, x, y))] x[P(x) & y x ((Q(x, y) v R(a, x, y))] x[P(x) & y t(Q(t, y) v R(a, t, y)] x[P(x) & q t(Q(t, q) v R(a, t, q))] xq t [P(x) & (Q(t, q) v R(a, t, q))].

    Контрольное задание. Найти предварённую нормальную форму для следующих формул.

    P(x)v(xQ(x,z)& yR(y,z));

    x (Q(x,z) ®R(x,t))vyt (P(y,t)

    S(y));

    x(P(x,z) ÛQ(x,z)) ®xz(R(x,z)®S(x,z).
    2. Сколемовская и клаузальная формы

    Для того, что бы легче и эффективнее было доказывать невыполнимость формулы или некоторого их множества, устанавливают ещё более строгие пределы использования механизма квантификации. Каждой формуле А сопоставляется некоторая формула SA c гарантией, что формулы либо обе выполнимы, либо обе невыполнимы. (SA  А). Форма SA называется сколемовской формой для соответствующей формулы А.

    Сколемовская форма – это такая предварённая форма, в которой исключены кванторы существования.

    Сколемовское преобразование (исключение -квантификации):

    сопоставить каждой -квантифицированной переменной список -квантифицированных переменных, предшествующих ей, а также некоторую ещё не использованную функциональную константу, число мест у которой равно мощности списка.

    В матрице формулы заменить каждое вхождение каждой
    -квантифицированной переменной на некоторый терм. Этот терм является функциональной константой со списком аргументов, соответствующих предшествующим -квантифи-цированным переменным и называется сколемовской функцией.

    Устранить из формулы все -квантификации.
    Пример1. Пусть формула имеет вид:

    uvwxyz M(u, v, w, x, y, z).

    Ей соответствует сколемовская форма:

    vxyM(a, v, f(v), x, y, g(v, x, y))

    где w заменена на f(v) и zнаg(v, x, y) – сколемовские функции.

    Пример 2. Найти сколемовскую форму и сколемовские функции для предикатной формулы xyz wt (S(x,y,y)(S(z,v,x)&P(w,t,t))), если S(x,y,z)=(x+y=z), P(x,y,z)=(x*y=z) – предикаты суммы и произведе­ния соответственно.

    Решение: 1) преобразование импликации:

    xyz wt (S(x,y,y) (S(z,v,x)&P(w,t,t))),

    2) Выполним сколемовское преобразование, пусть z = f(x, y), w =g(x, y)

    SA: xy t (S(x, y, y) (S(f(x,y), g(x,y), x) & P(g(x,y), t, t))),

    3) Найдём сколемовские функции:

    f(x, y) + g(x, y)=x и g(x,y)* t = t, следовательно g(x,y)=1и f(x,y)=1–t.

    Клаузальной формой называется такая сколемовская форма, матрица которой является КНФ. Любая сколемовская форма допускает эквивалентную клаузальную форму.


    написать администратору сайта