Минимален ербранов модел на множество от положителни хорнови клаузи

Минимален ербранов модел на множество от положителни хорнови клаузи

нека P е множество от положителни хорнови клаузи;

нека C = A :– B₁, B₂ …, B_n е затворен частен случай на C

( е някаква субституция); казваме, че затворената формула

A е непосредствено изводима чрез C от B₁, B₂ …, B_n;

База: всички аксиоми, съответни на P са изводими от P;

Предположение: нека C = A :– B₁, B₂, …, B_n, n > 0, C  P;

нека C е затворен частен случай на C и

B₁, B₂, …, B_n са изводими от P;

Стъпка: тогава A е изводима от P;

Заключение: няма други изводими формули от P;
съвсем лесно се проверява, че всички изводими формули от P са затворени;
примери:

нека P = { parent (mincho, ivan), male (mincho), male (ivan),

distinct (X, Y) :– parent (X, Y) };

ясно е, че ако T и U са затворени термове, то distinct (T, U) е непосредствено изводима от parent (T, U);

например distinct (mincho, ivan) е изводима от P, тъй като е непосредствено изводима от parent (mincho, ivan), която пък е аксиома, съответна на P;

нека имаме следната сигнатура – константа zero, едноместен функционален символ s и едноместен предикатен символ even;

нека P = { even (zero), even (s (s (X)) :– even (X) };

тогава изводимите от P формули са:

even (zero), even (s (s (zero))), even (s (s (s (s (zero))))), …;
нека S_P е ербрановата структура, в която са вярни всички изводими от P формули и само те;
Теорема: S_P е модел на P;

Доказателство: нека F  P; ако F е атомарна формула, то всички затворени частни случаи на F са аксиоми, съответни на P  всички затворени частни случаи на F са изводими от P  всички затворени частни случаи на F са вярни в S_P, но S_P е с термално породен носител  F е тъждествено вярна в S_P;

нека F има вида A :– B₁, B₂, …, B_n, n > 0; нека F е произволен частен случай на F ( e някаква субституция); имаме

F = A :– B₁, B₂, …, B_n; ще покажем, че F е верен в S_P;

достатъчно е да покажем, че ако B₁, B₂, …, B_n са вярни в S_P,

то A е вярна в S_P; действително, ако B₁, B₂, …, B_n са

вярни в S_P, то B₁, B₂, …, B_n са изводими от P  A също е изводима от P  A е вярна в S_P; така всеки затворен частен случай на F е верен в S_P и S_P е с термално породен носител 

F е тъждествено вярна в S_P;

Доказателство: нека A е затворена атомарна формула, която е вярна в S_P; тогава A е изводима от P;

нека S е произволен модел на P; с индукция по дефиницията за изводимост ще покажем, че A е вярна в S;

База: ако A е аксиома, съответна на P, т.е. A = B, където B е атомарна формула от P, то A е вярна в S, тъй като B е тъждествено вярна в S  всеки затворен частен случай на B е верен в S;

Предположение: нека C  P, C = B :– B₁, B₂, …, B_n, n > 1, A = B,

B₁, B₂, …, B_n са изводими от P и за тях е изпълнено твърдението, т.е. те са вярни в S;

Стъпка: C е тъждествено вярна в S  всеки затворен частен случай на C е верен в S  B :– B₁, B₂, …, B_n =

= A :– B₁, B₂, …, B_n е вярна в S  импликацията

B₁ & B₂ & … & B_n  A е вярна в S, но B₁, B₂ …, B_n са

вярни в S  B₁ & B₂ & … & B_n е вярна в S  A е вярна в S;

то G е изпълнима при P;

G е изпълнима във всеки модел на P, т.е. G е изпълнима при P;

ясно е, че една затворена атомарна формула е вярна във всеки модел на P  тази формула е вярна в S_P; така S_P е ербрановата структура, в която са вярни всички затворени атомарни формули, които са вярни във всеки модел на P и само те;

ако една хорнова цел G е изпълнима при P, то някой затворен частен случай на G е верен във всеки модел на P;

Доказателство: G е изпълнима при P  G е изпълнима във всеки модел на P; в частност G е изпълнима в S_P и тъй като S_P е с термално породен носител, то съществува частен случай G на G, който е верен в S_P; нека G = B₁ & B₂ & … & B_n, n  0;

тогава G = B₁ & B₂ & … & B_n; тъй като G е вярна в S_P, то

B₁, B₂, …, B_n са вярни в S_P; от горното твърдение

B₁, B₂, …, B_n са вярни във всеки модел на P 

G = B₁ & B₂ & … & B_n е вярна във всеки модел на P, т.е.

G е частен случай на G, който е верен във всеки модел на P;

тогава M има модел  тялото на никоя клауза от M\P не е изпълнимо при P;

Доказателство: нека M има модел S; нека C е произволна отрицателна хорнова клауза, C  M\P,

C = :– B₁, B₂, …, B_n, n  0, C  (B₁ & B₂ & … & B_n);

тъй като C е тъждествено вярна в S  (B₁ & B₂ & … & B_n) е тъждествено вярна в S  B₁ & B₂ & … & B_n не е изпълнима в S;

така S е модел на P, в който тялото на C не е изпълнимо 

тялото на C не е изпълнимо при P;

нека тялото на никоя отрицателна хорнова клауза от M\P не е изпълнимо при P; ще покажем, че M има модел;

разглеждаме структурата S_P; нека C  M;

ако C  P, то C е тъждествено вярна в S_P, тъй като S_P е модел на P;

нека C  M\P, C = :– B₁, B₂, …, B_n, n  0, C  (B₁ & B₂ & … & B_n);

ще покажем, че B₁ & B₂ & … & B_n не е изпълнима в S_P;

да допуснем, че B₁ & B₂ & … & B_n е изпълнима в S_P; тъй като S_P има термално породен носител, то съществува частен случай

B₁ & B₂ & … & B_n, който е верен в S_P  B₁ & B₂ & … & B_n е верен във всеки модел на P  B₁ & B₂ & … & B_n е изпълнима във всеки модел на P, т.е. B₁ & B₂ & … & B_n е изпълнима при P, което е противоречие; така B₁ & B₂ & … & B_n не е изпълнима в S_P 

(B₁ & B₂ & … & B_n) е тъждествено вярна в S_P  C е тъждествено вярна в S_P; така S_P е модел на M;
примери: нека сигнатурата, която използваме се състои от една константа a, един едноместен функционален символ f и един едноместен предикатен символ p;

нека P = { p (a), p (f (f (X))) :– p (X) };

да разгледаме хорновата цел G = p (f (a));

една структура, в която G не е изпълнима е структурата с носител множеството от естествените числа, константата a е интерпретирана с 0, предикатният символ p е интерпретиран с предиката за четност, функционалният символ f – с добавяне на 1;

при тази структура G = p (f (a)) означава, че 1 е четно число, което очевидно не е вярно; ще подходим към въпроса за

изпълнимост на G при P по друг начин; ще покажем, че G не е изпълнима в S_P  G не е изпълнима при P; трябва да покажем,

че никой частен случай на G не е верен в S_P, т.е. изводим от P;

G има единствен частен случай – себе си, тъй като G е затворена формула; ясно е, че затворените термове в дадената сигнатура са

fⁿ (a) за n = 0, 1, … (с fⁿ (a) означаваме ;

има единствена аксиома, съответна на P – p (a);

затворените частни случаи на другата клауза са p (f (f (T))) :– p (T), където T е затворен терм; така изводимите формули в P са

p (a), p (f (f (a))), …, т.е. p (fⁿ (a)), където n е четно число;

при това положение G не е вярна в S_P, тъй като G = p (f¹ (a));

така G не е изпълнима при P;

да разгледаме друга хорнова цел G = p (X) & p (f (X));

затворените частни случаи на G имат вида

G [X/fⁿ (a)] = p (fⁿ (a)) & p (fⁿ⁺¹ (a)); при това положение, никой затворен частен случай на G не е верен в S_P, тъй като n и n+1 са с различна четност  G не е изпълнима в S_P 

G не е изпълнима при P;