.RU

 - формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т.е. F = 


 - формулой, если она представлена в ПНФ и содержит только кванторы всеобщности, т.е.

F = x1x2 xn (M).

Для устранения кванторов существования из префикса формулы разработан алгоритм Сколема, вводящий сколемовскую функцию для связывания предметной переменной квантора существования с другими предметными переменными.


2.1.5.1 Алгоритм Сколема

Шаг 1. Представить формулу F в виде ПНФ, т.е.

F=x1x2xn(M), где i{; }Шаг 2. Найти в префиксе самый левый квантор существования:

a) если квантор находится на первом месте префикса, то вместо переменной, связанной кван­тором существования, подставить всюду предметную по­стоянную a , отличную от встречающихся предметных постоянных в матрице формулы, а квантор существования удалить;

б) если квантор находится не на первом месте префикса, т.е. x1x2xi-1xi .., то выбрать (i-1)-местный функциональный символ, отлич­ный от функциональных символов матрицы М и выполнить замену предметной переменной xi, связанной кванто­ром существования, на функцию f(x1;x2 ; xi-1 ) и квантор существования удалить.

Шаг 3. Найти следующий справа квантор существования и перей­ти к исполнению шага 2, иначе конец.

Формулу ПНФ, полученную в результате введения сколемовской функции называют сколемовской стандартной формой формулы (ССФ).

Пример:

F=x1x2x3x4x5x6 ((P21 (x1; x2) P32(x3; x4; x5))P 23(x4; x6)).

1) заменить предметную переменную x1 на постоянную a:

F=x2x3x4x5x6 ((P21. (a; x2)P32.(x3; x4; x5))P23 (x4; x6));

2) заменить предметную переменную x4 на функцию f2 1.(x2;x3):

F=x2x3x5x6 ((P21.(a; x2)P32 (x3; f 21(x2; x3); x5))P23 (f21(x2; x3); x6));

  1. заменить предметную переменную x6 на функцию

f32(x2; x3 ; x5 ):

F=x2x3x5((P21(a; x2)P32(x3; f21(x2; x3); x5))

P23(f21(x2; x3);f32(x2; x3 ; x5 ))).

К={(P21(a; x2)P32(x3; f21(x2; x3); x5)); P23(f21(x2; x3);f32(x2; x3 ; x5 ))}.


2.2. Исчисление предикатов

Все методы и результаты исчисления высказываний можно перенести на исчисление предикатов, т. е. каждая теорема и любой вывод исчисления высказываний становятся теоремой и выводом исчисления предикатов, если пропозициональные переменные заменить формулами языка предикатов, причем все вхождения одной и той же переменной везде заменить одной и той же формулой. Каждая схема теоремы и каждая схема вывода также сохраняются, если под знаками пропозициональных переменных принимать формулы языка предикатов.

Для того, чтобы формализовать процесс рассуждения в исчислении предикатов, необходимо выделить класс фор­мул, определяющих их эквивалентные преобразования при наличии кванторов, и класс отношений между формулами формирующих последователь­ную цепь формул от посылок до заключения. Следует отметить, что правила, аксиомы и законы исчисления высказываний есть подмножество правил, аксиом и законов исчисления предикатов. Дополнительные пра­вила, аксиомы и законы определяют возможности введения и удаления кванторов, подстановки и cмeны кванторов.


2.2.1 Интерпретация формул

Под интерпретацией следует понимать систему, состоящую из не­пустого множества V, называемом универсумом, и однозначного отображения на двухэлементное множество {и; л}, кото­рое каждому предикатному символу Pn (t1; t2; tn ) ставит в соот­ветствие n - местное отношение на множестве V, каждому функциональному символу f ni (t1; t2; tn ) - n-местную операцию на множестве V, каждой предметной постоянной - элемент множе­ства V.

При заданной интерпретации предметные переменные рассматриваются как переменные, пробегающие область универсума V, а символам логических и кванторных операций придается их обычный смысл.

Например, если универсум задан множеством целых чисел, то для x y z (P2 (+(x, y); z)):= “существуют числа x, y, z, для которых z больше суммы чисел х и у", то при х=2, у=3, z=10 имеем двухместную операцию =5 и двухместное отношение между целым числом 10 и значением операции +(2,3)=5. Отображение P2(5;10) на двухэлементное множество дает значение “и”. При х=2, у=3, z=4 имеем +(2,3)=5 и P2 (5; 4)=л.

На рис. 10 приведена графическая интерпретация этой задачи.















P2 (5; 4)



Рис.10 Интерпретация x y z (P2 (+(x, y); z)) для x=2, y=3, z=10 или z=4.


Другими словами, интерпретация функциональных символов опре­деляется по значениям функции на универсуме, заданном на множестве термов, входящих аргументами в эту функ­цию, а интерпретация предикатных символов по отображению на двухэлементное множество {и; л}.

Особо следует рассмотреть влияние свободных переменных на интерпретацию формул исчисления предикатов.

Формула, не содержащая свободных переменных, называется замк­нутой и представляет собой высказывание об элементах, функциях и отношениях, которое принимает значение и или л. На рис. 10 рассмотрен случай замкнутой формулы.

Формула, содержащая свободные переменные, называется открытой и представляет собой отношений, заданное на множестве V,

Это отношение может быть истинным для одних значений из области интепретации и ложным для других.

При такой интерпретации выделяют три класса формул, тождест­венно истинные, тождественно ложные и выполнимые.

Тождественно истинные формулы (или тавтологии) -это особый класс формул исчисления предикатов, которые принимают значение “истины” для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов; эти формулы иг­рают роль законов и аксиом исчисления предикатов; любые подстановки и замещения в тождественно истинной формуле не изменяют ее значения.

Например,

для предиката P2(x, y):=”число x меньше числа y” формула xy(P2(x, y)):=”для любого целого числа x найдется число y, большее числа x” является тождественно истинной;

для любой F(x) формула x(F(x))x(F(x)):=“формула ”существуют x, для которых F(x)=и”, эквивалентна формуле “не для всех x F(x)=л”” является тождественно истинной.

Тождественно ложные формулы (или противоречие)-это особый класс формул исчисления предикатов, которые принимают значение “ложь” для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов; любые подстановки и замещения в тождественно ложной формуле не изменяют ее значения.

Например, для предиката P2(x, y):=”число x меньше числа y” формула xy(P2(x, y)):=”существует целое число x, которое меньше любого целого числа y” является тождественно ложной;

для любой F(x) формула x(F(x))x(F(x)):=”“существует x, для которой F(x)=и”, и “для всех x F(x)=л ”” является тождественно ложной.

Выполнимые формулы - это особый класс формул исчисления преди­катов, которые принимают значение “истина”в некоторой области, т.е. не для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула x(F(x))x(F(x)) является истинной для одного элемента множества V и ложной для всех элементов этого множества, т.к.

x(F(x))x(F(x)):=” если существует x, для которого F(x)=и, то не для всех х универсума F(x)=и” .


2.2.2 Правила вывода

Вывод заключения из множества посылок записывается так же, как в исчислении высказываний

F1;F2;Fn B, где слева от знака “” записывают множество формул посылок и необходимые аксиомы F1;F2;Fn, а справа – формулу заключения B. Тогда знак “” означает “верно, что B выводима из F1;F2;Fn.

Отношение логического вывода эквивалентно теореме

F1;F2;FnB.

Другая форма записи : F1; F2;Fn

B,

где над чертой записывают множество посылок и аксиом F1;F2;Fn, а под чертой заключение B.

Для организации вывода заключения из множества посылок используют правила подстановки и правила заключения.


2.2.2.1 Правила подстановки

Если в формулу F(х), содержащей свободную переменную x, выполнить всюду подстановку вместо x терма t , то получим формулу F(t).

Этот факт записывают так:

xtF(x)

F(t).


Подстановка некоторого терма t в формулу F(x) вместо ее свободной переменной x состоит в замещении всех свободных вхождений этой переменной данным термом t. Такая подстановка называется правильной. Подстановка будет неправильной если в результате подстановки сколемовской функции свободная переменная окажется в области действия квантора.

Например,

1. x1x2x3( P21(x1, x3) P2 (x2))

x3( P21(x2, x3) P2 (x2)).

Это правильная подстановка, т.к. x1 –свободная переменная.

2. x1f(x2, t) x3( P21(x1, x3) P2 (x2))

x3( P21(f(x2, t), x3) P2 (x2)).

Это - правильная подстановка, т.к. x1 –свободная переменная.




3. x3x2x3( P21(x1, x3) P2 (x2))

x3( P21(x1, x2) P2 (x2)).

Это - неправильная подстановка, т.к. x3 –связанная квантором .

4. x2x3x3( P1(x1, x3) P2 (x2))

x3( P1(x1, x3) P2 (x3)).

Это - неправильная подстановка, т.к. предикат P2 (x3) попадает в область действия квантора .

Понятие правильной подстановки необходимо, например, для формулировки законов снятия квантора общности

x F(x)

F(t)


и введения квантора существования

F(t)

xF(x).


2.2.2.2 Правила введения и удаления кванторов

Наиболее распространенными правилами являются:

1) Введение квантора общности: “если F1(t) F2(x) выводимая формула и F1(t) не содержит свободной переменной x , то F1(t) x(F2(x)) также выводима”, т.е.

(F1(t) F2(x))

(F1(t) x(F2(x))).

2) Удаление квантора общности: "если x(F(x)) выводимая формула, то вместо x можно выполнить подстановку терма t, свободного от x , и получить также выводимую формулу F (t), т.е.

x(F(x))

. F (t).

3) Введение квантора существования: "если терм t вхо­дит в предикат F(t) , то существует, по крайней мере одна предмет­ная переменная x , удовлетворяющая требованиям x(F(x)) ”, т.е.

F(t)

x(F(x)).

  1. 4) Смена квантора:

x(F(x)) x(F(x))

x(F(x)); x(F(x)).

  1. 5) Перенос квантора, если терм t не содержит переменной x:

a) x(F1(x)) F2(t)

x(F1(x) F2(t));

b) x(F1(x))F2(t)

x(F1(x) F2(t);

c) F1(t) x(F2(x))

x(F1(t)F2(x));

d) x(P(x))F(t)

x(P(x)F(t));


e) x(P(x))F(t)

x(P(x)F(t)).

6) Введение новой переменной:

a) x(F1(x))x(F2(x))

yx(F1(y) F2(x));

b) x(F1(x))x( F2(x))

yx(F1(y) F2(x)).


2.2.2.3 Правила заключения

Существует два основных правила определения истинности заключения:

а) если F1 и (F1F2) выводимые фор­мулы, то F2 также выводима. Это - правило modus ponens (m.p).

F1; (F1F2)

F2.

b) если F2 и (F1F2) выводимые формулы, то F1 также. выводима. Это - правило modus tollens (m.t).

F2; (F1F2)

F1.


Эти правила определяют схему вывода и позволяют использовать правила подстановки, введения и удаления кванторов и делать вывод об истинности заключения.


2.2.3 Метод дедуктивного вывода

В логике предикатов вывод определяется так же, как в исчислении высказываний. Все правила вывода логики высказываний включены в множество правил логики предикатов.

Пример: “Таможенные чиновники обыскивают каждого, кто въезжает в страну, кроме высокопоставленных лиц. Если некоторые люди способствуют провозу наркотиков, то на внутреннем рынке есть наркотик. Никто из высокопоставленных лиц не способствовает провозу наркотиков. Следовательно, некоторые из таможников способствуют провозу наркотиков?”

Пусть P1(x):=”x - таможенный чиновник”, P2(x,y):=”x обыскивает y”, P3(y):=”y въезжает в страну”, P4(y):=”y – высокопоставленное лицо”, P5(y):=”y способствует провозу наркотиков”.

y(P3(y)P4(y)x(P1(x)P2(x,y)));

y(P3(y)P5(y));

y(P3(y)P4(yP5(y));

x(P1(x)P5(x)).

1) F1= y(P3(y)P5(y)) - посылка;

2) F2=P3(a)P5(a) - заключение по формуле F1 и правилу удаления квантора существования;

3) F3= P3(a) - заключение по формуле F2 и правилу удаления логической связки конъюнкции;

4) F4= P5(a) - заключение по формуле F2 и правилу удаления логической связки конъюнкции;

5) F5=y(P3(y)P4(yP5(y)) посылка;

6) F6= P3(t)P4(tP5(t) - заключение по формуле F5 и правилу удаления квантора общности;

7) F7=P3(t)P4(t)P5(t) - заключение по формуле F6 и ее эквивалентным преобразованиям;

8) F8=P4(a) - заключение по формуле F7 при t=a для P3(a)=л и P5(a)=л;

9) F9=y(P3(y)P4(y)x(P1(x)P2(x,y))) - посылка;

10) F10=yx (P3(y)P4(y) (P1(x)P2(x,y))) - заключение по формуле F9 и правилу приведения к ПНФ;

11) F11=P3(a)P4(a)P1(t)P2(t,a) - заключение по формуле F10 и правилу удаления квантора общности;

12) F12= P3(a)P4(a) - заключение по формулам F3 и F8 и правилу введения логической связки конъюнкции исчисления высказываний;

13) F13=(P1(t)P2(t,a)) - заключение по формулам F11 и F12 и правилу modus ponens;

14) F14= P1(t) -заключение по формуле F13 и правилу удаления логической связки конъюнкции исчисления высказываний;

15) F15=P5(a)=P5(t) -заключение по формуле F4 и замене предметной постоянной термом;

16) F16= P1(t)P5(t) -заключение по формулам F14 и А15 и правилу введения логической связки конъюнкция исчисления высказываний;

17) F17=x(P1(x)P5(x)) -заключение по формуле F16 и правилу введения квантора существования. Так доказана истинность формулы x(P1(x)P5(x)).

y(P3(y)P4(y)x(P1(x)P2(x,y)))

y(P3(y)P4(yP5(y));


y(P3(y)P5(y))




yx (P3(y)P4(y) (P1(x)P2(x,y)))

P3(t)P4(tP5(t)


P3(a)P5(a)

P3(a)P4(a) P1(t)P2(t,a)





P3(t)P4(t)P5(t)

P3(a)

P5(a)

(P1(t)P2(t,a))






t
P4(a)

P1(t)
=a


P3(a)P4(a)


a=t
P1(t)P5(t)

P5(t)





x(P1(x)P5(x))


Рис. 11. Граф вывода заключения

Пример: Доказать истинность заключения

x( P1(x)( P2(x))); x(P3(x)P1(x))

x(P3(x)( P2(x))).

1) F1=x( P1(x)( P2(x))) - посылка;

2) F2=x(P3 (x)P1 (x)) -посылка;

3) F3=(P1 (t)( P2 (t))) - заключение по формуле F1 и правилу 2) удаления квантора общности;

4) F4= P3 (t) P1 (t) - заключение по формуле F2 и правилу 2) удаления квантора общности;

5) F5= (P3 (t)( P2 (t))) - заключение по формулам F3, F4 и закону силогизма исчисления высказываний (см 1.2.3.2 правило 11);

6) F6=x(P3(x)(P2(x))) - заключение по формуле F5 и правилу 1 введения квантора общности.

Так доказана истинность формулы x(P3(x)(P2(x))).

На рис. 12 приведен граф, иллюстрирующий процесс дедуктивного вывода.


x( P1(x)( P2(x)))

x(P3 (x)P1 (x))



(P1 (t)( P2 (t)))

P3 (t) P1 (t)




(P3 (t)( P2 (t)))



x(P3(x)(P2(x)))

Рис. 12. Граф вывода заключения




Пример: Доказать истинность заключения

x(y(P21.(x; y)P2(y))y((P3(y) P24.(x; y))); x(P3(x))

x(P3(x))xy(P21.(x; y)(P2(y))).


1) F1=x(y(P21.(x; y)P2(y))y((P3(y) P24.(x; y))) - посылка;

2) F2= x(P3(x)) -посылка;

3) F3=x(P3(x)) - заключение no формуле F2 и правилу 5) смены кванторов (закон де Моргана);

4) F4=P3 (t) - заключение по формуле F3 и правилу 2) удаления квантора общности;

5) F5=P3(t)P24.(x;t) - заключение по формуле F4 и правилу 4) исчисления высказываний;

6) F6=y(P3(y)(P24 (x; y))) - заключение по формуле F5 и правилу 1) введения квантора общности;

7) F7=y(P3(y)P24 (x; y)) - заключение по формуле F6 и правилу смены кванторов (закон де Моргана);

8) F8=y(P21.(t; y)P2(y)y(P3(y)P24.(t; y)) - заключение по формуле F1 и правилу 2) удаления квантора общности;

9) F9= y(P21.(t; y)P2(y)) - заключение пo формулам F7 и F8 при условии t=x и правилу modus tollens;

10) F10=y( P21.(t; y)P2(y)) - заключение по формуле F9 и правилу смены кванторов (закон де Моргана);

11) F11=y(P21. (t; y) (P2 (y)) - заключение пo формуле F10 и эквивалентным преобразованиям алгебры предикатов;

12) F12=xy(P21. (x; y) (P2 (y)) - заключение по формуле F11 и правилу 1) введения квантора общности;

13) x(P3(x))xy(P21.(x; y)( P2(y))) – заключение по формулам F2 и F12 и правилу modus ponens. Что и требовалось доказать.


 x(P3(x))

x(y(P21.(x; y)P2(y))y((P3(y) P24.(x; y)))
На рис. 13 приведен граф вывода этой задачи.






x(P3(x))

y(P21.(t; y)P2(y)y(P3(y)P24.(t; y))





P3 (t)

 y(P21.(t; y)P2(y))



P3(t)P24.(x;t)

y( P21.(t; y)P2(y))



y(P21. (t; y) (P2 (y))

y(P3(y)(P24 (x; y)))



y(P3(y)P24 (x; y))

xy(P21. (x; y) (P2 (y))




x(P3(x))xy(P21.(x; y)( P2(y)))



рис. 13 Граф вывода заключения

Пример. Доказать истинность заключения

x(P1(x)y(P2(y)P24.(x; y))); x(P1(x)y(P3(y)P24.(x; y)))

x(P2(x)P3(x)).


1) F1=x(P1(x)y(P2(y)P24.(x; y))) - посылка;

2) F2=x(P1(x)y(P3(y)P24 (x; y))) - посылка;

3) F3=P1(а)y(P2(y)P24.(a; y)) -заключение по формуле F1, правилу формирования ССФ;

4) F4=P1(a)- заключение по формуле F3 и правилу удаления конъюнкции исчисления высказываний

5) F5=y(P2(y) P24.(a; y)) - заключение пo формуле F3 и правилу удаления конъюнкции исчисления высказываний;

6) F6=P2(t) P24.(a; t) - заключение по формуле F5 и правилу 2) удаления квантора общности;

7) F7=P1(t)y(P3(y)P24 (t; y)) - заключение по формуле F2 и правилу 2) удаления квантора общности;

8) F8=y(P3(y) P24 (a; y)) - заключение по формулам F3 и F7 при t=a и правилу modus ponens;

9) F9=P3(t)P24.(a; t) - заключение по формуле F8 и правилу 2) удаления квантора общности;

10) F10=P24.(a; t)P3(t) - заключение по формуле F9 и закону контрапозиции (правило 8) исчисления высказываний);

11) F11=P2(t)P3(t) - заключение по формулам F6 и F10 и закону силлогизма (правило 11) исчисления высказываний);

12) F12=x( P2 (x)P3(x)) - заключение по формуле F11 и правилу 1) введения квантора x. Что требовалось доказать.

На рис. 14 приведен граф вывода этой задачи.

x(P1(x)y(P2(y)P24 (x; y)))

x(P1(x)y(P3(y)P24.(x; y)))




x=a


P1(а)y(P2(y)P24.(a; y))

P1(t )y(P3(y)P24 (t; y))



P1(a)

y(P2(y) P24.(a; y))

P1(a )y(P3(y)P24 (a; y))







y(P3(y) P24 (a; y))

P2(t) P24.(a; t)



P3(t)P24.(a; t)



P24.(a; t)P3(t)






P2(t)P3(t)



x( P2 (x)P3(x))

Рис. 14. Граф вывода заключения




2.2.4 Принцип резолюции

Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpuменим алгоритм принципа резолюции, рассмотренный в исчислении высказываний. Этот алгоритм основывается на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами ) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых ) атома с разными знаками, то из них можно получить третий дизъюнкт , который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.

Например, если даны два дизъюнкта (P1(x)P2(x)) и (P1(f(x))P3(y)), то для получения контрарной пары атомов возможна подстановка

xf(х)(P1(x)P2(x))=(P1(f(x))P2(f(x))) и

xf(х)(P1(f(x))P3(y))= (P1(f(x))P3(y)).

В результате склеивания этих дизъюнктов может быть получена резольвента: (P1(f(x))P2(f(x)))(P1(f(x))P3(y))= (P2(f(x)) P3(y)).

Если пара дизъюнктов имеет вид (P1(f1(x))P2(x)) и (P1(f2(x))P3(y)), то никакая подстановка не позволит сформировать резольвенту.


Пример: Даны две формулы P3(a;x;f(q(y))) и P3(z;f(z);f(u)).

Выполнить унификацию контрарных атомов.

1) za P3(z;f(z);f(u))=P3(a;f(a);f(u));

2) xf(a) P3(a;x;f(q(y)))=P3(a;f(a);f(q(y)));

3) uq(y) P3(a;f(a);f(u))=P3(a;f(a);f(q(y))).

В результате получены два контрарных атома: P3(a;f(a);f(q(y))) и P3(a;f(a);f(q(y))). Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постоянной b, т.е.

ybP3(a;f(a);f(q(y)))=P3(a;f(a);f(q(b))) и

ybP3(a;f(a);f(q(y)))= P3(a;f(a);f(q(b))),

то получим два контрарных высказывания.

Пример. Даны две формулы P3(x;a;f(q(a))) и P3(z;y;f(u)).

Выполнить унификацию контрарных формул.

1) xbP3(x;a;f(q(a)))=P3(b;a;f(q(a)));

2) ya P3(z;y;f(u))=P3(z;a;f(u));

3) yaP3(z;a;f(u))=P3(b;a;f(u));

4) uq(a)P3(b;a;f(u))=P3(b;a;f(q(a))).

В результате получены две контрарных формулы: P3(b;a;f(q(a))) и P3(b;a;f(q(a))).

Принцип резолюции может быть усилен линейным выводом, упорядочением атомов в дизъюнкте и использо­ванием информации о резольвируемых атомах.

Линейным выводом из множества дизъюнктов K называется последовательность дизъюнктов D1, D2,...Dn, где каждый член DiK, а каждый Di+1 является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества K.

Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом Pj старше атома Pi в упорядоченном дизъюнкте тогда и только тогда, когда j > i. Например, в упорядоченном дизъюнкте (P1P2P3P4) младшим считается атом P1, а старшим - P4. При наличии в упорядоченном дизюънкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.

Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Од­нако они несут полезную информацию. Поэтому вмес­то удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший - сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т.е.получить пустой дизъюнкт.

Пример: Суждение “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следавательно, некоторые преподаватели были аспирантами.” [1] Пусть P1(x):=”x – отличник”, P2(x):=”x – аспирант”, P3(x):=”x –студент”, P24 (x; y):=”x сдает зачет y”, P5(x):=”x – преподаватель”. Формулы этого суждение имеют вид:

x(P3(x)P1 (x)y(P5(y)P24 (x; y))); x(P2(x)P3(x)y(P24 (x; y)P2 (y)));

x(P2(x)P1(x)) .

x(P5(x)P2(x)).

1) F1=x(P3(x)P1 (x)y(P5(y)P24 (x; y)))=

xy(P3(x)P1 (x)(P5(y)P24 (x; y)))=

x(P3(x)P1 (x)(P5(f(x))P24 (x; f(x)))).

M1=(P3(x)P1 (x)P5(f(x))P24 (x; f(x)))=

(P3(x)P1 (x)) P5(f(x))P24 (x; f(x)) =

(P3(x)P1 (x) P5 (f(x))P24 (x; f(x))=

(P3(x)P1 (x) P5(f(x)))(P3(x)P1 (x) P24 (x; f(x))).

2) F2=x(P2(x)P3(x)y(P24 (x; y)P2 (y)))=

xy(P2(x)P3(x)(P24 (x; y)P2 (y)))=

y(P2(a)P3(a)(P24 (a; y)P2 (y))).

M2=(P2(a)P3(a)(P24 (a; y)P2 (y)))=

P2(a)P3(a)(P24 (a; y)P2 (y))).

3) F3=x(P2(x)P1(x)).

M3=(P2(x)P1(x))= (P2(x)P1(x)).

4) F4=x(P5(x)P2(x))= x( (P5(x)P2(x))).

M4=( (P5(x)P2(x)))= (P5(x) P2(x))).
K= {(P3(x)P1 (x)P5(f(x))); (P3(x)P1 (x) P24 (x; f(x))); P2(a); P3(a); ^ (P24 (a; y)P2(y)); (P1(x)P2(x)); (P5(x)P2(x))};



1
P2(a)
) xa (P1(x)P2(x))  P2(a)= P1(a) = P1(a);

2
P1(a)
)P1(a)xa(P3(x)P1 (x)P24 (x; f(x)))= P3(a) P24 (a; f(a));

3
P1(a) 1(a)
) P3(a)  P24 (a; f(a)) yf(a) (P24 (a; y)P2(y))=


P1(a)

P24 (a; f(a))
P3(a)  P2(f(a));


P1(a)

P24 (a; f(a))
4) P3(a)  P2(f(a)) xf(a)(P5(x)P2(x))=


P1(a)

P24 (a; f(a))

P2(f(a))
P3(a)  P5(f(a));


P1(a)

P24 (a; f(a))

P2(f(a))
5) P3(a)  P5(f(a)) 

x
P1(a)

P5(f(a))

P2(f(a))

P24 (a; f(a))
a(P3(x)P1 (x)P5(f(x)))= P3(a)     P1 (a);


P1(a)

P24 (a; f(a))

P2(f(a))

P5(f(a))
6) P3(a)    P1 (a)P1(a)=


P1(a)

P1(a)

P24 (a; f(a))

P2(f(a))

P5(f(a))
P3(a)    =


P1(a)
P3(a);


P1(a)

P1(a)

P3(a)
7) P3(a)  P3(a)=  = .


На рис. 14 дан граф линейной унификации этого примера.


P1(x)P2(x)

P1(a) P2(a)


P1(a)
P3(a) P24 (a; f(a)) P3(x)P1 (x)P24 (x; f(x))


P24 (a; f(a))

P1(a)
P3(a)  P2(f(a)) P24 (a; y)P2(y)


P1(a)

P24 (a; f(a))

P2(f(a))
P3(a)    P5(x)P2(x)


P2(f(a))

P24 (a; f(a))

P1(a)
P5(f(a))

P3(a)   P3(x)P1 (x)P5(f(x))


P1(a)

P5(f(a))
 P1 (x)

P3(a) P1(a)

Рис. 14. Граф линейной унификации


Пример: Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один из преподавателей не является невеждой. [1]

Пусть P1(x):=” x – студент”, P2(y):=”y – преподаватель”, P23(x, y):=”x любит y”, P4(y):=”y - невежда”.

Формулы этого суждение имеют вид:

x(P1(x)y(P2 (y)P23(x; y)));

x(P1(x) y(P4 (y)P23(x; y)));

y(P2 (y)P4(y));

  1. F1=x(P1(x)y(P2 (y)P23(x; y)))= xy(P1(x) (P2 (y)P23(x; y)))= y(P1(a) (P2 (y)P23(a; y)))= y(P1(a) (P2 (y)P23(a; y)));

M1= P1(a)(P2 (y)P23(a; y));

  1. F2=x(P1(x) y(P4 (y)P23(x; y)))=

xy (P1(x)  (P4 (y)P23(x; y)))= xy (P1(x)P4 (y)P23(x; y)));

M2=(P1(x)P4 (y)P23(x; y));

  1. F3=y(P2 (y)P4(y))= y((P2(y)P4(y))= y(P2(y) P4(y))=

P2(b)P4(b);

M3=P2(b)P4(b).
K={P1(a); (P2 (y)P23(a; y)); (P1(x)P4 (y)P23(x; y)); P2(b); P4(b)};


P2(b)
1) P2(b)  xb(P2 (y)P23(a; y))= P23(a; b);


P2(b)
2) P23(a; b)yb (P1(x)P4 (y)P23(x; y))=


P2(b)
P23(a; b)(P1(x)P4 (b)P23(x; b));

3
P2(b)
) P23(a; b)xa(P1(x)P4 (b)P23(x; b))=

4
P2(b)

P23(a; b)
)  P1(a)P4 (b) P1(a)=


P2(b)

P23(a; b)

P1(a)
  P4 (b);

5
P2(b)

P23(a; b)

P1(a)
)   P4 (b) P4(b)=


P2(b)

P23(a; b)

P1(a)

P4 (b)
  = .


На рис. 15 приведен граф линейной унификации для этого примера.

P2(b)


P2(b)

P2(b)
P23(a; b) P2 (y)P23(a; y)

P23(a; b) (P1(x)P4 (b) P1(x)P4 (y)P23(x; y)


P2(b)
P23(x; b))


P23(a; b)

P1(a)
 P1(a) P4 (b) P1(x)P4 (b)P23(x; b))


P2(b)

P23(a; b)
  P4 (b) P1(a)

 P4(b)

Рис. 15. Граф линейной унификации


2.3 Проблемы в исчислении предикатов

Для обоснования исчисления предикатов, как для любой аксиоматической теории, необходимо рассмотреть проблемы разрешимости и непротиворечивости.

Проблема разрешимости исчисления предикатов есть проблема поиска эффективной процедуры в доказательстве. Исчисление предикатов – пример неразрешимой формальной системы, т.к. нет единого эффективного алгоритма в доказательстве любой формулы. Наличие кванторов, ограничивающих области определения, наличие сколемовских функций не позволяет использовать таблицы истинности.

Проблема непротиворечивости исчисления предикатов заключена в доказательстве невыводимости формулы и ее отрицания. Исчисление предикатов непротиворечиво, т. к. каждая доказуемая формула является тождественно истинной формулой. Тогда ее отрицание является тождественно ложной формулой и при доказательстве в исчислении предикатов ведет к противоречию.


2.4 Логическое программирование

Типичным представителем языка программирования для описания последовательности действий в процессе логического вывода является Prolog.

Пролог-программа состоит из предложений, которые бывают трех типов: факты, правила и вопросы.

Левая часть правила - - есть формализованное описание заключения, а правая часть правила – - формализованное описание условий, определяющих истинность вывода заключения, т.е.

:-”.”

Символ “:-“ соответствует символу обратной импликации ””.

Если множество условий имеют между собой конъюнктивную связь, то между ними ставится запятая, т.е.

:-{“,”}”.”.

Если условия имеют между собой дизъюнктивную связь, то между ними ставится точка с запятой, т.е.

:-{“;”}”.”.

На языке Prolog эти правила записывают так:

:-

”,”

”;”

”.”

Голова предложения при написании программы всегда сдвинута влево относительно перечня условий. Каждое условие начинается с новой строки.

Смысл этого правила таков:“если истинны условия 1 и 2 или 3, то истинно и заключение ”.

Предметные переменные и предметные постоянные являются аргументами заключения и условий.

Если тело пусто, то голова есть истинное утверждение или аксиома. Факты –это предложения, имеющие пустое тело.

”.”.

Если голова пуста, то тело продставляет вопрос, т.е.

? - ”.”.

С помощью вопросов пользователь может спрашивать систему о том, какие утвреждения являются истинными или ложными. Предметные переменные, включаемые в вопросы, сравниваются с помощью правил с предметными постоянными, вкючаемыми в факты, и система формирует ответ.

Например, множество правил для определения степени родства:

дед(X, Y):-

родитель(X, Z),

родитель(Z, Y).

брат(X, Y):-

родитель(Z, X),

потомок(X; U; Z, Y):-

родитель(Y, Z),

родитель(Z, U),

родитель(U, X).

родитель(Z, Y).

можно применить к родословной русских князей X века:

отец(игорь, святослав).

отец(святослав,владимир).

отец(владимир, борис).

отец(владимир,глеб).

?-дед(святослав, Y).

Y=борис.

Y=глеб.

?-брат(X, Y).

X=борис.

Y=глеб.

?-потомок(X; Y; Z, игорь).

Z=святослав.

U=владимир.

X=борис.

X=глеб.

Предметные переменные заключения, как правило, связаны квантором общности, а для условий - квантором существования. Например, правило “дед(X, Y):- родитель(X, Z), родитель(Z, Y)” утверждает, что если для всех X и Y существует Z, то X -дед для Y.

Правило “брат(X, Y):-родитель(Z, X), родитель(Z, Y)” утверждает, что если для всякого X и Y существует общий Z, то X брат Y.

Рассмотренный метод обобщает механизм унификации. Аргументы вызова это имена переменных, которые подставляют на место формальных параметров. Формальными параметрами могут быть термы. Поэтому процесс вызова включает совмещение термов, яляющихся аргументами вызова с термами из заголовка.

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


Контрольные_вопросы.

1) Запишите символически следующие суждения:

a) "все судьи - юристы, но не все юристы – судьи”;

б) "лица, проходившие ранее подготовку в аспирантуре, ис -пользовавшие отпуск для завершения диссертации как соискатели или бывшие в творческом отпуске для завершения диссертации, правом поступления в аспирантуру не пользуются".

в) “Судья, являющийся родственником потерпевшего, не может участвовать в рассмотрении дела. Судья X - родственник потерпевшего. Следовательно, судья X не может участвовать в рассмотрении дела.”[5]

г) “К уголовной ответственности привлекаются лица, совершившие тайное похищение личного имущества граждан. Обвиняемый X не совершал тайного похищения личного имущества граждан. Следовательно, обвиняемый X не может быть привлечен к уголовной ответственности”.

д) “Если иск предъявлен недееспособным лицом, то суд оставляет иск без рассмотрения. Иск предъявлен недееспособным лицом. Следовательно, суд оставляет иск без рассмотрения”.

2) Привести к предваренной нормальной форме:

a) (xy(P21.(x; y))(xy(P22.(x; y)));

б) (xy(P21.(x; y))(xy(P22.(x; y)));

в) (xy(P21.(x; y))(xy(P22.(x; y)));

г) xyzu(P(x, y, u, z).

3) Привести к сколемовской стандартной форме:

a) (xy(P21.(x; y))(xy(P22.(x; y)));

б) (xyzw(P4.(x; y; z; w));

в) (xy(P21.(x; y))(xy(P22.(x; y)))).

  1. Какие из нижеприведенных формул являются тождестивенно истинными:

  1. x(P1(x))x(P2.(x))x(P1(x)P2.(x));

б) y(P1.(x))y (P2.(x))y(P1.(x)(P2.(x));

в) x(P1(x)P2.(x))x(P1(x))x(P2.(x));

г) y(P1.(x)(P2.(x))y(P1.(x))y (P2.(x))

5) Докажите выводимость заключения методом дедукции:

a) x(P1.(x) P2.(x)); x(P3.(x)P1.(x))

x(P3.(x) P2.(x));


б) x(y(P21.(x; y)P2.(y) y(P3.(y)P24.(x; y)))

 x(P3.(x)xy(P21.(x; y) P2.(y)));


в) x(P1.(x)P2.(x) P3.(x)); x(P1.(x) P4.(x))

x(P4.(x)P3.(x)).

6) Докажите выводимость заключения по принципу резолюции:


a) x(P1.(x)y(P2.(y) P23.(x; y)));

x(P1.(x)y(P4.(y)  P23.(x; y)))

y(P2.(y)P4.(y)).


б) y(P1 (y)P2.(y))

x(y(P1.(y) P23.(x; y)) y(P2.(y) P23.(x; y))).


в) x((P1.(x)P2.(x))y(P3.(y)P24.(x;y)));

x(P5.(y) P1.(x) y(P24.(x;y)P5.(y)));

x(P3.(x) P5.(x)).

^ Расчетно-графическая работа

Найти формулы ПНФ и ССФ, выполнить унификацию атомов дизънктов.

Вариант

Формула

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

x( A(x)y(B(y)))( B(y)A(x))

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

x(A(x)B(y))yz((C(z)A(x))(C(z)B(y)))

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

x(A(x)B(x))y(B(x)C(y))z(C(y)D(z)))

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))



Литература


  1. Вагин В.Н. Дедукция и обобщение в системах принятия решений.- М.: Наука, 1988г. – 384 с.

  2. Войшвилло Е.К., Дектярев М.Г. Логика как часть теории познания и научной методологии. кн.1. Учебное пособие. –М.: Наука, 1994г. –312с.

3. Зегет В. Элементарная логика. - М.: Высшая школа, 1985г..- 256 с.

4. Кириллов В.И., Старченко А.А. Логика. - М.: Высшая школа, 1987г.– 271с.

5. Kузнецов О.П., Андельсон-Вельский Г.М. Дискретная матема­тика. для инженера.- М.: Энергоатомиздат, 1988г.—480 с.

6. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, матeмaтичecкoй логике и теории алгоритмов 240с.

7. ЛихтарниковЛ.М., Сукачева Т.Г. Математическая логика /курс лекций/ - СПб.: “Лань”, 1998г..-288с.

8. Першиков В.И., Савинков В.М. Толковый словарь по информатике – М.: Финансы и статистика, 1991г. –543с.

9. Пономарев В.Ф. Математические методы и модели в обработке информации и управлении. Методические разработки по разделу “Формальные системы”- Калининград: КГТУ, 1992г..

10. Роберт P. Столл. Множества. Логика. Аксиоматические теории.- М.: Просвещение, 1968. – 231 с.


Предметный указатель

Аксиомы исчисления высказываний, 45, 49

Алгебра высказываний, 7

Алгебра предикатов, 92

13-perechen-klyuchevih-dejstvij-po-vipolneniyu-meropriyatij-s-planovimi-srokami-ih-vipolneniya.html
13-povishenie-effektivnosti-individualnogo-i-kollektivnogo-truda-zhenshin-v-processe-optimizacii-ih-deyatelnosti.html
13-principi-ocenki-i-upravleniya-sistemami-kachestva-na-promishlennih-predpriyatiyah.html
13-puzir-vospriyatiya-skazka-o-sile.html
13-rossijskij-opit-rozhkov-g-v-r63-genezis-innovacionnoj-ekonomiki-v-rossii-pod-red-sgeroshenkova.html
13-smart-card-development-kit-sdk-diplomnaya-rabota.html
  • college.bystrickaya.ru/2-analiz-izmeritelnih-signalov-kak-sluchajnih-funkcij-uchebnoe-posobie-sankt-peterburg-2006-udk-778-5-nesterova.html
  • lesson.bystrickaya.ru/sobachij-nyuh.html
  • shpargalka.bystrickaya.ru/v-stoimost-vklyucheni-sleduyushie-uslugi-lenoblast-g-sestroreck-opisanie.html
  • shpora.bystrickaya.ru/www-powerlifting-kurgan-narod-ru-stranica-22.html
  • laboratornaya.bystrickaya.ru/razmer-otchislenij-v-rezerv-rasschitivaetsya-obshestvom-v-prilozhenii-k-uchetnoj-politike.html
  • upbringing.bystrickaya.ru/kontrolnie-voprosi-uchebnoe-posobie-k-kursu-yuridicheskaya-psihologiya-dlya-studentov-obuchayushihsya-po-specialnosti.html
  • vospitanie.bystrickaya.ru/zayavlenie-i-zhaloba-kratkij-konspekt-lekcij-2009-g-batichko-v-t-prokurorskij-nadzor-konspekt-lekcij-2009-g.html
  • crib.bystrickaya.ru/informacionnij-byulleten-mezhdunarodnoj-nezavisimoj-associacii-trezvosti.html
  • predmet.bystrickaya.ru/sorok-shest-richard-bah.html
  • books.bystrickaya.ru/chastyu-poryadok-formirovaniya-spravochnik-s-kommentariyami-k-federalnomu-zakonu-ot-6-oktyabrya-2003-goda-131-fz-ob.html
  • zadachi.bystrickaya.ru/the-american-revolution-essay-research-paper-what.html
  • zadachi.bystrickaya.ru/tablica-v4-zakusochnie-obshego-tipa-i-specializirovannie-metodicheskie-rekomendacii-po-discipline-organizaciya.html
  • school.bystrickaya.ru/groshova-sistema-rosjsko-mper-na-terenah-ukrani-u-xviii-xix-stoltt.html
  • write.bystrickaya.ru/glava-7-kitajskaya-filosofiya-uroki-mudrosti.html
  • writing.bystrickaya.ru/avtomatizaciya-zvuka-r-v-seredine-slov-avtomatizaciya-zvuka-r-v-slovah.html
  • vospitanie.bystrickaya.ru/zaklyuchenie-zaharova-i-g-338-informacionnie-tehnologii-v-obrazovanii-ucheb-posobie-dlya-stud-vissh-ped-ucheb-zavedenij.html
  • studies.bystrickaya.ru/gumanizaciya-otnoshenij-mladshih-shkolnikov-chast-4.html
  • learn.bystrickaya.ru/glava-13-o-podlinnih-sobstvennikah-gosudarstvennoj-vlasti-izdanie-2-e-ispravlennoe-i-dopolnennoe.html
  • tasks.bystrickaya.ru/33-okazanie-gosudarstvennoj-uslugi-predostavlenie-oficialnoj-statisticheskoj-informacii-po-zaprosam-grazhdan-i-organizacij-v-elektronnom-vide.html
  • literatura.bystrickaya.ru/s-odaryonnimi-detmi-reglamentiruyutsya-zakonom-yaroslavskoj-oblasti-ot-12-07-2004-goda-24-z-o-podderzhke-odarennih-detej-postanovleniem-gubernatora-yaroslavskoj-oblasti-ot-07-12-2004-g-stranica-13.html
  • otsenki.bystrickaya.ru/rossijskij-sovet-plan-raboti-prezidiuma-rossijskogo-soveta-profsoyuza-i-apparata-profsoyuza-na-ikvartal-2010-goda.html
  • exchangerate.bystrickaya.ru/kriminalistika-chast-33.html
  • textbook.bystrickaya.ru/itogi-i-perspektivi-tezisi-mezhdunarodnogo-seminara-10-11-oktyabrya-2001-goda-stranica-3.html
  • pisat.bystrickaya.ru/sushnost-upravleniya-i-menedzhmenta-zakoni-i-principi-menedzhmenta-vidi-menedzhmenta.html
  • college.bystrickaya.ru/16052010vlastinet-kishinev-moldaviyarossijskie-podrostki-bednee-amerikanskih-no-lenivee.html
  • lecture.bystrickaya.ru/5-funkciya-hristianstva-29-ii-otveti-na-nekotorie-voprosi-30-stranica-30.html
  • zadachi.bystrickaya.ru/programma-obucheniya-dolzhnostnih-lic-i-specialistov-go-i-tp-rschs-chuvashskoj-respubliki-v-gou-dpo-umc-gz-ina-kursah-go-i.html
  • teacher.bystrickaya.ru/glava-14-konflikti-socialnih-interesov-l-a-nikitich-glavnij-redaktor-izdatelstva.html
  • upbringing.bystrickaya.ru/meropriyatiya-gimnazicheskogo-festivalya-vozmyomsya-za-ruki-druzya.html
  • education.bystrickaya.ru/12-aprelya-2012g-uchitel-fiziki-utibkalieva-zhanglen-miraleevna.html
  • credit.bystrickaya.ru/polozhenie-oprovedenii-otkritogo-turnira-po-hudozhestvennoj-gimnastike-zolotaya-lenta-2011.html
  • universitet.bystrickaya.ru/traktorlar-zhne-olardi-bazasinda-zhasalan-zdiginen-zhretin-shassiler-men-mehanizmder-zdiginen-zhretin-auil-sharuashilii-meliorativtik-zhne-zhol-rilis-mashinalari-men-mehanizmder.html
  • uchitel.bystrickaya.ru/razrabotka-vneklassnogo-meropriyatiya-vo-2klasse.html
  • obrazovanie.bystrickaya.ru/prilozhenie-9-ob-utverzhdenii-sanitarnih-pravil.html
  • holiday.bystrickaya.ru/monitori-s-diagonalyu-17-19-dyujmov-kuznecov-s-l-deloproizvodstvo-na-kompyutere.html
  • © bystrickaya.ru
    Мобильный рефератник - для мобильных людей.