Тема 2.1.4 Перевод выражений логики предикатов в клаузальную форму.

Общая трудоемкость 11 часа, из них 6 час – аудиторные занятия, 5 ч - самостоятельные занятия.

В ходе аудиторных занятий студенты изучают алгебру предикатов, процесс получения предваренной, замкнутой, сколемовской и клаузальных нормальных форм логики предикатов [1], глава IV, параграф 7.

Задачи для самоконтроля по теме 2.1.4:

. Найти предваренную и клаузальную нормальные формы формул.

Вариант	Формула
1	x(A(x) B(y))y(B(y) A(x))
2	x( A(x)x( C(x)))x((C(x)A(x))
3	x(A(x)x(B(x)))y( A(x) C(y)C(y)B(x))
4	x(A(x)x(B(y)))x( A(x) B(y))
5	x(A(x)B(y))y(A(x)(B(y)C(z))z(A(x)C(z))
6	x(A(x)y(B(y)C(z)))z(A(x)B(y)C(z))
7	x(A(x)B(z))y(C(y)A(x))z(C(y)B(z))
8	x(A(x)B(y))y((C(y)A(x))(C(y)y(B(y)))
9	x(A(x)B(y))y(A(x)(B(y)C(z)))(A(x)z(C(z)))
10	x(A(x)B(y)A(x)y(B(y)C(z)))(A(x)z(C(z)))
11	x(A(x)z(B(y)C(z)))y(B(y)(A(x)C(z)))
12	(x(A(x))x(B(x)))z((B(x)C(z))(A(x)C(z)))
13	(x( A(x))x( B(x)))( B(x)A(x))
14	(x(A(x)))(x(B(x)))y(C(y)A(x)C(y)B(x))
15	ч( Ф(ч)н(И(н)))( И(н)Ф(ч))
16	(x(B(x))x(A(x)))y((A(x)C(y))( C(y)B(x)))
17	x( A(x)y(B(y)))(B(y)A(x))
18	x( A(x)y( B(y)))(B(y)A(x))
19	x(A(x)B(x))y(B(x)C(y)z(C(y)D(z)))
20	(x(A(x)B(x))z(C(z)A(x)))y(C(z)B(y))
21	(x(B(x)y(A(y)))(y(B(y)(A(x)C(z))))z(C(z))
22	x(B(x))y(A(y)B(x))
23	x(A(x)B(x))(y(C(y)A(x))z(C(z)B(x)))
24	x(B(x)A(y))(B(x)y(A(y)C(z)))z(C(z)))
25	x(A(x)B(z))y(C(y)A(x)z(C(y)B(z)))
26	(x(B(x))x(A(x)))(A(y)yC(y))( A(x)C(y))
27	(x(A(x))x(B(x)))y((A(x)C(y))(B(x)C(y)))
28	x(A(x)y(B(y)))( A(x)y(B(y)))B(y)
29	x(A(x)y(B(y)))( A(x)B(x))B(x)
30	x( A(x))(A(x)y(B(y)))
31	(x(B(x))x(A(x)))( B(x)A(x))A(x)
32	(x(B(x))x(C(x)))(A(y)B(x)A(y)C(x))
33	ч(Ф(ч)И(н))ня((С(я)Ф(ч))(С(я)И(н)))
34	(x(A(x))x(C(x)))y(C(x)B(y))(A(x)B(y))
35	x(A(x))y(B(y))y(C(y)xD(x))(A(x)C(y)) D(y))
36	x(A(x))( A(x)y(B(y)))
37	x(B(x))y(A(y)B(x))
38	x(B(x)y(A(y)))y(B(y)(A(x)C(z)))z(B(z) C(z))
39	x(B(x)A(y))(B(x)y(A(y)C(z)))z(B(x)C(z))
40	x(A(x)B(x))y((C(y)A(x))(C(y)B(x)))
41	(x( A(x)y( C(y)))(C(x)A(x))
42	x(A(x) B(y))y(B(y) A(x))
43	x(A(x)B(z))y((C(y)A(x))z(C(y)B(z)))
44	x(A(x)B(y))z(C(z)A(x))y(C(z)B(y))
45	ч(Ф(ч)И(ч))н(И(ч)С(н))я(С(н)В(я)))
46 46	x( A(x)y( B(y)))(B(x)A(x))
47	x( A(x)x(B(x)))(B(x)A(x))
48	(x(B(x)y(A(y))))y(A(x)C(y)) C(y)B(x)
49	(x( A(x)y(B(y))))( B(x)A(x))
50	x(A(x)B(y))y(A(x)(B(y)C(z)))z(A(x)C(z))