Вопрос 6. Метод резолюций в ив. Правило согласия. Метод резолюций для

Хорновских дизъюнктов.

D1=D’1 v A, D2=D’2 v­­­­A тогда резольвента: res(D1,D2)=D’1 v D'2( по литере А),

а res (A, A) (по литере А ) = 0

УТВЕРЖДЕНИЕ: Если res(D1,D2)=D’1 v D'2 существует, то секвенция

D1, D2 ├ res(D1,D2) доказуема

ДОКАЗАТЕЛЬСТВО: D1=1, D2=1 => в D1 или D2 истиной является другая литера=>

res(D1,D2)=1

S={D1,…,Dm}- множество дизъюнктов, последовательность дизъюнктов f1, …. , fn называется резолютивным выводом из множества S, если для любого i выполняется

fi € S или fi=res(fj , fk), где j, k <I

ТЕОРЕМА (о полноте метода резолюций)

Множество дизъюнктов S - противоречиво( секвенция S├ доказуема)  существует резолютивный вывод из S ? который заканчивается 0 (противоречием)

ТЕОРЕМА Если S – множество дизъюнктов содержащее все свои резольвенты, то S противоречиво  0 € S

Правило СОГЛАСИЯ

K1= K’1 ٨ A , K2= K’2 ^ ‾A ,¬ res по А(K1, K2) = K’1 ^ K’2, ¬res (A,¬A)=1

ТЕОРЕМА о полноте

Множество конъюнктов S = {K1, … ,K2} общезначно, (т е ╞ K1 v …. V Km)

 существует вывод из S по правилу согласия, который заканчивается на 1 .

ХОРНОВСКИЕ ДИЗЪЮНКТЫ

Дизъюнкт D называется Хорновским, если D содержит не более одной положительной литеры

S – множество хорновских дизъюнктов. Противоречиво ли S?

0 ¢ S => выбираем из S факт , дизъюнкт С, содержащий ¬P

res (C , P) = вычеркиваем из С литеры ¬P

S:=(S\{C})U({res(C,P)}, процесс продолжается до вывода 0, или стабилизируется на некоторое множество Хорновских дизъюнктов, не содержащее 0

Вопрос 7. Алгебраические системы. Формулы сигнатуры Подформулы. Свободные и связанные переменные. Предложения. Истинность формулы на элементах алгебраической системы.

Алгебраическая система сигнатуры  - пара € = A,  , где каждому предиксному символу p⁽ⁿ⁾   сопоставлено некоторое n – местное отношение на A, а каждому функциональному символу fⁿ   - n местная операция на A.

Атомарные формулы сигнатуры :

1. если t₁, …, t_n  T(  ), то t₁  t₂ – атомарная формула сигнатуры 

2. если t₁, …, t_n  T(  ), p^{( n )}  , то p(t₁, …, t_n) – атомарная формула сигнатуры 

3. других формул нет.

Формулы сигнатуры 

1. любая атомарная формула сигнатуры  является формулой сигнатуры 

2. если и  - формулы сигнатуры , x  V, то ( ), ( ), ( ), ^ x  ,  x  - формулы сигнатуры .

3. других формул нет.

формула сигнатуры SF() – множество подформул 

1. если атомарная формула, то SF() – SF() = 

2. если _ _, _ _ или _ _, то SF(₁)  SF(₂)

3. если ^_x _или  x _, то SF() = SF(₁)  {₂}

 = {F⁽²⁾, P⁽¹⁾}

Вхождение переменной Х в формулу называется связанным, если Х входит в терм или предикат, который находится в области действия квантора X или X. Вхождение переменной называется свободным, если оно не является связанным. Переменная Х называется связанной (свободной), если некоторое ее вхождение связанное (свободное).

Предложение называется формула, не имеющая свободных переменных.

1. z  x(y R(x, y)^p(x)); z – фиктивная переменная

2. y  x(R(x, y)^x Q(x))

y  x(R(x, y)^z Q(z))

, FV()  {x₁, x₂, …, x_n}

Формула (х₁, …, х_n) сигнатуры  называется тождественно истиной или общезначимой (тождественно ложной или противоречивой), если для любой алгебраической системы  = A,  и любых a₁, …, a_nA выполняется ╞ (a₁, …, a_n). (╞ (a₁, …, a_n).)

Формула (х₁, …, х_n) называется выполнимой (опровержимой), если для нек. = A,  и нек. a₁, …, a_nA выполняется ╞ (a₁, …, a_n).