Задачи 2_ 3_ 4 (1162126)

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

Текст из файла

3. ∀x (P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃z R(x, z))Tφ = h∅ | ∀x (P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃z R(x, z))iR→∨T1 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x) ∨ ∀x∃z R(x, z)iR∨∨T2 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x), ∀x∃z R(x, z)iR∀∨T3 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x), ∃z R(c1 , z)i∨ L∀φ1*+z}|{T4 = ∀x (P (x) → ∃y R(x, f (y))), P (c1 ) → ∃y R(c1 , f (y)) | ∃x ¬P (x), ∃z R(c1 , z)L→L→∨∨T4.1 = hφ1 , ∃y R(c1 , f (y)) | ∃x ¬P (x), ∃z R(c1 , z)iT4.2 = hφ1 , | ∃x ¬P (x), ∃z R(c1 , z), P (c1 )iL∃R∃∨T5.1 = hφ1 , R(c1 , f (c2 )) | ∃x ¬P (x), ∃z R(c1 , z)iR∃∨T5.2 = hφ1 , | ∃x ¬P (x), ∃z R(c1 , z), P (c1 ), ¬P (c1 )i∨∨DT5.1 = φ1 , R(c1 , f (c2 )) | ∃x ¬P (x), ∃z R(c1 , z), R(c1 , f (c2 ))Закрытые таблицыEDET5.2 = φ1 , P (c1 ) | ∃x ¬P (x), ∃z R(c1 , z), P (c1 )Здесь A, B — формулы логики предикатов,Γ, ∆ — множества формул логики предикатов,x — предметная переменная, c — константа,t — терм.L¬h¬A, Γ | ∆iR¬hA&B, Γ | ∆iR&hA, B, Γ | ∆iL∨hA ∨ B, Γ | ∆ihA → B, Γ | ∆iR∨h∀x A, Γ | ∆iR→R∀hA{x/c}, Γ | ∆iгде константа c не содержитсяв формуле A, а также вформулах множеств Γ и ∆hΓ | A → B, ∆ihΓ | ∀x A, ∆ihΓ | A{x/c}, ∆iгде переменная x свободнав формуле A для терма th∃x A, Γ | ∆ihΓ | A ∨ B, ∆ihA, Γ | B, ∆ihA{x/t}, ∀x A, Γ | ∆iL∃hΓ | A&B, ∆ihΓ | A, B, ∆ihB, Γ | ∆i; hΓ | A, ∆iL∀hΓ | ¬A, ∆ihΓ | A, ∆i; hΓ | B, ∆ihA, Γ | ∆i; h B, Γ | ∆iL→Таблица закрыта, еслиhΓ | ∆i, Γ ∩ ∆ 6= ∅hA, Γ | ∆ihΓ | A, ∆iL&R6где константа c не содержитсяв формуле A, а также вформулах множеств Γ и ∆R∃hΓ | ∃x A, ∆ihΓ | A{x/t}, ∃x A, ∆iгде переменная x свободнав формуле A для терма t3Нормальные формы и унификация3.13.2Преведение к ССФНахождение НОУP (t1 , t2 , .

. . tn )→= P (s1 , s2 , . . . sn )1. Переименование переменных|= ∃∀ x F (x) ≡ ∃∀ y F (y)2. Уничтожение импликаций |= (A → B) ≡ (¬A ∨ B)1.f (t1 , t2 , . . . tn )= f (s1 , s2 , . . . sn )→t1 = s1t2 = s2..........tn = sn(b) |= (¬ ∃∀ xF (x)) ≡ ( ∀∃ x¬F (x)2.f (t1 , t2 , .

. . tn )= f (s1 , s2 , . . . sk )→НОУ не существует(c) |= ¬¬A ≡ A3. ti = xi→x1 = t i4. ti = ti→∅3. Отрицания∨(a) |= ¬(A &∨ B) ≡ (¬A & ¬B)4. Вынос кванторов|= ∃∀ xF (x) &∨ B ≡∃ x(F (x) &∨∀B)5. xi = ti5. |= A & B ∨ C ≡ (A ∨ C) & (B ∨ C)4t1 = s1t2 = s2..........tn = sn(ti 6= xi )(xi ∈/ V arti , ∃k xi ∈ V artk )6. xi = ti(xi ∈ V arti )→→Во все tk подствить вместо xi tiНОУ не существует// можно: X/c, X/f(c), X1/f(X2), f(X1, X2, X3) = f(Y1, Y2, Y3)// нельзя: c/X, c1/c2, X1 = f(X1), f(X1, X2, X3) = f(Y1, Y2)Метод резолюцийУпражнение 4.1Упражнение 4.21.

¬P (f (x, y), z, h(z, y)) ∨ R(z, v), Q(x) ∨ P (f (y, x), g(y), v)D1 = ¬P (f (x, y), z, h(z, y)) ∨ R(z, v)D2 = Q(x) ∨ P (f (y, x), g(y), v)НОУ(P (f (y, x), g(y), v), ¬P (f (x, y), z, h(z, y))) f (y, x) = f (x, y) f (y, x) = f (x, y)31g(y)=zz=g(y) −→−→v== h(z, y)v== h(z, y)y=xx=yz=g(y)v = = h(z, y)5−→y=xz=g(x)v = = h(z, x)5−→y=xx=xz=g(x)v = = h(z, x)4−→1. S = {D1 , D2 , D3 , D4 , D5 }D1D2D3D4D5= P (X1 , f (X1 ))= R(Y2 , Z2 ) ∨ ¬P (Y2 , f (a))= ∨R(c, X3 )= R(X4 , Y4 ) ∨ R(Z4 , f (Z4 )) ∨ ¬P (Z4 , Y4 )= P (X5 , X5 )D6D1 ,D2={X1 /a,Y2 /a}D7D4={X4 /Z4 ,Y4 /f (Z4 )}D8D7 ,D3={X3 /f (c),Z7 /c}D9D1 ,D8={X1 /c}R(a, Z6 )R(Z7 , f (Z7 )) ∨ ¬P (Z7 , f (Z7 ))¬P (c, f (c))y=xz=g(x)v = = h(g(x), x)1.

∃x P (x) → ¬∀x ¬P (x)Θ = {y/x, z/g(x), v/h(g(x), x)}D3D1 ,D2=ΘR(g(x), h(g(x), x)) ∨ Q(x)Упражнение 4.3φ0 = ¬(∃x P (x) → ¬∀y ¬P (x))φ01 = ∃x P (x) & ∀y ¬P (y)φ02 = ∃x∀y P (x) & ¬P (y)φ1 = ∀y P (c) & ¬P (y)S = {P (c), ¬P (y)}D1 = P (c)D2 = ¬P (y)3. ∀x(P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃zR(x, z))D1 ,D2=D3{y/c}φ0 = ¬(∀x1 (P (x1 ) → ∃y1 R(x,1 f (y1 ))) → (∃x2 ¬P (x2 ) ∨ ∀x3 ∃z1 R(x3 , z1 )))φ01 = ∀x1 (¬P (x1 ) ∨ ∃y1 R(x1 , f (y1 ))) & ∀x2 P (x2 ) & ∃x3 ∀z1 ¬R(x3 , z1 )φ02 = ∀x1 ∃y1 ∀x2 ∃x3 ∀z1 (¬P (x1 ) ∨ R(x1 , f (y1 ))) & P (x2 ) & ¬R(x3 , z1 )2.

∃x∀yR(x, y) → ∀y∃xR(x, y)φ1 = ∀x1 ∀x2 ∀z1 (¬P (x1 ) ∨ R(x1 , f (g(x1 )))) & P (x2 ) & ¬R(h(x1 , x2 ), z1 )φ0 = ¬(∃x1 ∀y1 R(x1 , y1 ) → ∀y2 ∃x2 R(x2 , y2 ))S = {¬P (x1 ) ∨ R(x1 , f (g(x1 ))), P (x2 ), ¬R(h(x1 , x2 ), z1 )}φ01 = ∃x1 ∀y1 R(x1 , y1 ) & ∃y2 ∀x2 ¬R(x2 , y2 )φ02 = ∃x1 ∀y1 ∃y2 ∀x2 R(x1 , y1 ) & ¬R(x2 , y2 )D1 = ¬P (x1 ) ∨ R(x1 , f (g(x1 )))φ= ∀y1 ∀x2 R(c, y1 ) & ¬R(x2 , f (y1 ))1D2 = P (x2 )S={R(c, y1 ), ¬R(x2 , f (y1 ))}D = ¬R(h(x , x ), z )331323D4D1 ,D2={x1 /x2 }D5D3 ,D4={x4 /h(x31 ,x32 ),z3 /f (g(h(x31 ,x32 )))}D1 = R(c, y1 )D2 = ¬R(x2 , f (y2 ))R(x4 , f (g(x4 ))D3D1 ,D2={x2 /c,y1 /f (y2 )}переименование переменных.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов ответов (шпаргалок)