Логическо програмиране 2004/05 - упражнения

Казваме, че една формула е в пренексна нормална форма, ако тя е от вида $$Q_1 x_1 Q_2 x_2\ldots Q_n x_n \varphi$$, където $$\varphi$$ е безкванторна формула, а $$Q_i$$ са квантори.

Казваме, че една формула е в Скулемова нормална форма, ако тя е в пренексна нормална хорма и в нея участват само квантори за всяко ($$\forall$$).

Теорема на Скулем. За всяка логическа формула $$\varphi$$ на предикатното смятане от първи ред има формула $$\varphi'$$ в Скулемова нормална форма, така че за произволна структура S $$\varphi$$ е тъждествено вярна в S <-> $$\varphi'$$ е тъждествено вярна в S, т.е. можем да приведем всяка формула в Скулемова нормална форма като запазим тъждествената вярност.

Литерал наричаме атом (положителен литерал) или отрицание на атом (отрицателен литерал).

Алгоритъм за скулемизация

1. Премахват се всички еквивалентности: A <-> B = (A -> B) & (B -> A).
2. Премахват се всички импликации: A -> B = !A v B.
3. Ограничава се областта на отрицанието, така че да се получат литерали, т.е. отрицанието да не е пред квантор или пред скоби. Използват се законите на де Морган: !(A v B) = !A & !B, !(A & B) = !A v !B. Винаги се започва от най-външното отрицание, за да се избегнат излишни действия!
4. Преименуване на свързаните променливи, така че всеки квантор да е с различна променлива. Използва се факта, че Qx F = Qy F[x/y].
5. Изкарване на кванторите отпред (пренексна нормална форма) - използват се пренексните закони: Qx(A & B) = (QxA) & B и Qx(A v B) = (QxA) v B, за x не участваща в B. При изкарване на кванторите трябва да се внимава да не би да се разместят, т.е. Q₁x₁Q₂x₂... да не излезе като Q₂x₂Q₁x₁... Това не важи за квантори, чиито области на действие не се пресичат, например (Q₁x₁F) & (Q₂x₂G).
6. Скулемизация. Премахват се кванторите за съществуване по следните правила:
• свързаната променлива на квантор за съществуване, пред който няма квантори за всяко се заменя с нова константа
• свързаната променлива на квантор за съществуване, пред който има квантори за всяко $$\forall x_1\ldots\forall x_n$$ се заменя с терма f(x₁,...,x_n), където f е нов n-местен функционален символ.