Theorem proving method for ERM-model formal system.pdf Модель «Сущность - Связь - Отображение» или, сокращенно, ERM-модель(от английского «Entity - Relationship - Mapping») является семантической моде-лью данных и, обладая широким спектром выразительных возможностей, позво-ляет отразить большинство особенностей предметной области еще в рамках близ-кого человеку семантического моделирования [2]. Второй отличительной особен-ностью этой модели является наличие в ее основе теории семантически значимыхотображений (ТСЗО). Эта теория, доведенная до строгой математической фор-мальной системы, обеспечивает надежные правила проверки ERM-схем на проти-воречивость, безупречные правила пополнения ERM-схем дополнительными ог-раничениями целостности, вытекающими из ограничений целостности, заданныхнепосредственно проектировщиком, а также правила эффективной и полнойтрансформации ERM-схем в СУБД-ориентированные схемы (в частности - в ре-ляционную).Все эти правила базируются на аксиомах и доказанных теоремах формальнойсистемы ТСЗО. В предыдущих статьях [1, 3] предложены первоначальные вари-анты формальной системы. Нет ничего удивительного в том, что каждый вариантфиксирует некоторое текущее представление об этой системе, достаточное длярассмотренных на этом этапе теорем. По мере доказательства новых теорем про-исходит постоянное совершенствование правил построения формул и аксиомати-ческого базиса формальной системы. Каждая вновь доказанная теорема, с однойстороны, расширяет систему, обеспечивая базис для новых теорем, с другой сто-роны, позволяет совершенствовать набор упомянутых ранее правил ERM-модели.По-видимому, нет необходимости в дальнейшем обосновании важности дока-зательства новых теорем для развития ERM-модели. Настоящая статья предлагаетдетальное рассмотрение методики такого доказательства и послужит в качественаставления для настоящих и будущих исследователей ERM-модели.Формальная система ТСЗО построена на базе исчисления предикатов первогопорядка, доказательства теорем проводятся методом резолюций.114 А.М. Бабанов, А.С. Скачкова1. Высказывание гипотезы и формулировка теоремына языке формальной системы ТСЗОК настоящему моменту исследователями ERM-модели накоплен значительныйбанк гипотез ТСЗО, ожидающих своего доказательства. Одним из источниковэтих гипотез является непрекращающийся анализ закономерностей во взаимоот-ношениях между понятиями ERM-модели и ТСЗО. Другим важным источникомгипотез является теория реляционных БД, теоремы которой часто отражают такиезакономерности данных, которые можно выразить в терминах ТСЗО.Одним из важнейших понятий реляционной модели является понятие функ-циональной зависимости (ФЗ). Оно играет основную роль в процессе нормализа-ции отношений, определяет важный класс ограничений целостности. Выводи-мость одних и тех же ФЗ - важное условие эквивалентности двух схем. ФЗ выво-дятся в соответствии с аксиомами Армстронга, для удобства также используютсятри правила, являющиеся следствием этих аксиом. В ERM-модели есть понятие,очень близкое понятию «функциональная зависимость» - «функциональное ото-бражение». Взаимно-однозначное соответствие этих понятий позволяет получитьгипотезы и теоремы ТСЗО на основе аксиом Армстронга.В качестве примера, поясняющего методику доказательства, рассмотрим пра-вило декомпозиции ФЗ теории реляционных БД. Пусть A, B и C являются произ-вольными подмножествами множества атрибутов отношения R. Тогда, если име-ется ФЗ A  B,C, то справедливы ФЗ A  B и A  C.Формулировка теоремы декомпозиции ТСЗО, аналогичной правилу декомпо-зиции, будет выглядеть следующим образом. Если отображение со сложным об-разом функционально, функциональны и все его проекции на любые роли образови их совокупности.Для доказательства теоремы в первую очередь необходимо сформулироватьпосылку и заключение теоремы на языке нашей формальной системы - языке ис-числения предикатов первого порядка. Имена переменных и функторов вводятсяв соответствии с алфавитом формальной системы, описанной в [1].В нашем случае посылкой будет высказывание о функциональности исходногосложного отображения.Аксиома функциональности отображения в общем виде выглядит так:z/1,z/ 2,z/3(z/ 2 =ϕ(z/1)z/3 =ϕ(z/1)z/ 2 =z/3).Приведем ее к виду, соответствующему контексту теоремы. В данной теоремеречь идет об отображении со сложным образом, поэтому вместо z/2 и z/3, которые всоответствии с алфавитом формальной системы могут означиваться как просты-ми, так и сложными объектами, следует использовать y/1 и y/2 (они предназначеныдля переменных-агрегатов). В результате посылка теоремы примет следующийвид:y/1,y/ 2,z/1(y/1 =ϕ(z/1)y/ 2 =ϕ(z/1)y/1 =y/ 2).Это можно прочитать так: «Для любых y/1, y/2 и z/1, если y/1 и y/2 являются обра-зами z/1 при отображении ƒ, то они совпадают». В данном случае в качестве про-образа используется z./1, так как не принципиально, является ли он атомом или аг-регатом, индекс «/1» указывает на порядковый номер переменной - 1, порядковыйиндекс роли не имеет значения и поэтому не указан. Для обозначения образов вы-брано имя переменной y, что подчеркивает тот факт, что образы отображения ƒ вслучае нашей теоремы всегда являются сложными.Методика доказательства теорем для формальной системы ERM-модели 115В заключении теоремы говорится о функциональности проекции отображения.Конкретизируем аксиому функциональности, заменив отображение ƒ на его про-екцию на группу ролей образов 1. В соответствии с используемым алфавитомпроекция получит обозначение ƒ[>1]. При проекции на группу ролей 1 не важно,состоит эта группа из одной роли или нескольких, поэтому для обозначения обра-зов используется переменная z. Поскольку образами проекции являются объекты,играющие роль 1, индексы переменных для образов приобретают вид «1/1» и«1/2», где первая единица идентифицирует роль (группу ролей), а второе число -порядковый номер переменной. Соглашения об именовании переменных и функ-торов формальной системы помогают понять смысл выражений языка и избавля-ют от ошибок при формулировке теорем.Таким образом, заключение нашей теоремы примет следующий вид:/z1z1/1z1/ 2(z1/1 = ϕ[>1](z/1)z1/ 2 = ϕ[>1](z/1)z1/1 =z1/ 2).2. Определение необходимых для доказательствааксиом и теорем ТСЗОПрежде чем продолжить изложение методики доказательства теорем ТСЗОприведем уточненные выражения аксиом формальной системы ТСЗО.А к с и о м а р а в е н с т в а с о с т а в н ы х о б ъ е к т о вАксиома состоит из двух общезначимых формул, первая из которых говорит отом, что из равенства составных объектов следует равенство их соответствующихкомпонентов, вторая утверждает обратное.y/1y/ 2z1/1z2/1...zm/1z1/ 2z2/ 2...zm/ 2(y/1 = y/ 2 = y/1 =y/ 2 z1/1=z1/ 2z2/1 =z2/ 2...zm/1 =zm/ 2 ) иy/1y/ 2z1/1z2/1...zm/1z1/ 2z2/ 2...zm/ 2(y/1 =y/ 2 = z1/1=z1/ 2z2/1=z2/ 2...zm/1=zm/ 2 )y/1 =y/ 2 .А к с и о м а к о н к а т е н а ц и и о б ъ е к т о вНеобходимость в этой аксиоме обусловлена тем фактом, что в ТСЗО, в отли-чие от традиции, сложившейся в математике, множество, состоящее из двух мно-жеств, рассматривается как множество из их элементов. Эта аксиома также состо-ит из двух общезначимых формул:y/1y/ 2y/3z1/1z2/1...zm/1z1/ 2z2/ 2...zm/ 2(y/1 = y/ 2 = y/3 =y/3 =) иy/1y/ 2y/3z1/1z2/1...zm/1z1/ 2z2/ 2...zm/ 2(y/1 =y/ 2 = 116 А.М. Бабанов, А.С. Скачковаy/3 =y/3 =) .А к с и о м а и н в е р с и и :1z1 z2(z2 2 1(z1) z1 2 1(z2)) −  = ϕ> ↔ = ϕ> .А к с и о м а к о м п о з и ц и и :z1z3(z3= ϕ2>3(ϕ1>2(z1)) ↔ z2(z2 = ϕ1>2(z1) z3= ϕ2>3(z2))) .А к с и о м а о б ъ е д и н е н и я :z1z2 (z2 = (ϕ1>2/1 ϕ1>2/2 )(z1) ↔z2 = ϕ1>2/1(z1)z2 = ϕ1>2/2 (z1)) .А к с и о м а п е р е с е ч е н и я :z1z2 (z2 = (ϕ1>2/1 ϕ1>2/2 )(z1) ↔z2 = ϕ1>2/1(z1) z2 = ϕ1>2/2 (z1)) .А к с и о м а р а з н о с т и :z1z2 (z2 = (ϕ1>2/1 − ϕ1>2/2 )(z1) ↔z2 = ϕ1>2/1(z1) ¬z2 = ϕ1>2/2 (z1)) .А к с и о м ы п р о е к ц и й :- на i ролей образов:z1...mzm+1...m+i(zm+1...m+i = ϕ1...m>m+1...m+i...n[>m+1...m+i](z1...m)↔↔ ym+1...nzm+i+1...n(ym+1...n=ϕ1...m>m+1...m+i...n(z1...m)ym+1...n=)) ;- на j ролей прообразов:z1... jzm+1...n(zm+1...n= ϕ1...j...m>m+1...n[1...j>](z1... j )↔↔ y1...mzj+1...m(zm+1...n=ϕ1...j...m>m+1...n(y1...m)1... 1... 1... , )) m j j m y z z+  =< > ;- на i ролей образов и j ролей прообразов одновременно:z1... jzm+1...m+i(zm+1...m+i = ϕ1...j...m>m+1...m+i...n[1...j>m+1...m+i](z1... j )↔↔ y1...mym+1...nzj+1...mzm+i+1...n(ym+1...n=ϕ1...j...m>m+1...m+i...n(y1...m)1... 1... 1... , m j j m y z z+  =< >1ym+ ...n=)) .Поскольку порядок ролей не принципиален, мы позволили себе для проекцийиспользовать первые i ролей образов и первые j ролей прообразов.А к с и о м а а г р е г а т а :y23z1(y23=(ϕ1>2◊ϕ1>3)(z1)↔↔ z2z3(z2 = ϕ1>2(z1)z3 = ϕ1>3(z1)y23 =)).Методика доказательства теорем для формальной системы ERM-модели 117А к с и о м ы о б о т н о ш е н и я х и о т о б р а ж е н и я х :z1z2...zn(R(z1,z2,...,zn)↔↔y2...n(z1=ϕ2...n>1(y2...n )y2...n=)) ,…z1...zmzm+1...zn (R(z1,...,zm,zm+1,...,zn) ↔↔y1...mym+1...n(y1...m=ϕm+1...n>1...m(ym+1...n)y1...m= ym+1...n =)) ,…z1...zmzm+1...zn (R(z1,...,zm,zm+1,...,zn) ↔↔y1...mym+1...n(ym+1...n =ϕ1...m>m+1...n(y1...m)y1...m= ym+1...n =)) ,…z1z2...zn(R(z1,z2,...,zn)↔↔y2...n(y2...n=ϕ1>2...n(z1) y2...n=)) .А к с и о м а ф у н к ц и о н а л ь н о с т и о т о б р а ж е н и я :1 2 3 2 1 3 1 2 3 ) z/,z/ ,z/(z/ =ϕ(z/ )z/ =ϕ(z/ )z/ =z/ .А к с и о м а п о л н о т ы о т о б р а ж е н и я :z/1(z/1=экземпляр(ООО(ϕ))  z/ 2 (z/ 2 = ϕ(z/1))) .А к с и о м а с л е д с т в и я о т о б р а ж е н и й :z/1z/ 2(z/ 2=ϕ(z/1)z/ 2=ƒ(z/1)).А к с и о м а э к в и в а л е н т н о с т и о т о б р а ж е н и й :z/1z/ 2(z/ 2=ϕ(z/1)↔z/ 2=ƒ(z/1)).После уточнения аксиоматического базиса нашей формальной системы вер-немся к методике доказательства.Доказательство новых теорем базируется на аксиомах и уже доказанных тео-ремах ТСЗО. При этом для наглядности их обобщенные формулировки на языкеисчисления предикатов первого порядка видоизменяются с учетом контекста до-казываемой теоремы. Для нашей теоремы, кроме уже использованной в формули-ровке аксиомы функциональности, понадобятся также аксиома проекции и ак-сиома равенства сложных объектов.1. Аксиома проекции на i ролей образов:z1...mzm+1...m+i(zm+1...m+i = ϕ1...m>m+1...m+i...n[>m+1...m+i](z1...m)↔↔ ym+1...nzm+i+1...n(ym+1...n=ϕ1...m>m+1...m+i...n(z1...m)ym+1...n=)) .118 А.М. Бабанов, А.С. СкачковаВ данной теореме понадобится проекция на одну группу ролей образов. Такимобразом, аксиома примет следующий вид:z/1z1/1(z1/1 = ϕ[>1](z/1)↔ y/1z2/1(y/1 = ϕ(z/1)y/1 =)).2. Аксиома равенства сложных объектов:y/1y/ 2z1/1z2/1...zm/1z1/ 2z2/ 2...zm/ 2(y/1 = y/ 2 = y/1 =y/ 2 z1/1=z1/ 2z2/1 =z2/ 2...zm/1 =zm/ 2 ) .Для доказательства достаточно рассматривать ее вариант с размерностью кар-тежа m = 2. В таком случае аксиома будет выглядеть следующим образом:y/1y/ 2z1/1z2/1z1/ 2z2/ 2(y/1 =y/ 2 = y/1 =y/ 2 z1/1=z1/ 2z2/1 =z2/ 2 ) .3. Общие принципы доказательстваРамки статьи не позволяют подробно описать все детали метода резолюций,составляющего основу методики доказательства. Недостающую информациюможно получить в [4]. Мы же ограничимся лишь принципиальными моментами, восновном касающимися специфики применения метода резолюций в нашей мето-дике.Полную формулировку нашей теоремы составляют: общезначимые формулы аксиом- проекции - A1:z/1z1/1(z1/1 = ϕ[>1](z/1)↔ y/1z2/1(y/1 = ϕ(z/1)y/1 =)),- равенства сложных объектов - A2:y/1y/ 2z1/1z2/1z1/ 2z2/ 2(y/1 =y/ 2 = y/1 =y/ 2 z1/1=z1/ 2z2/1 =z2/ 2 ) ; предполагаемая истинной по условию теоремы посылка - A3:y/1,y/ 2,z/1(y/1 =ϕ(z/1)y/ 2 =ϕ(z/1)y/1 =y/ 2); заключение теоремы - B:z/1z1/1z1/ 2(z1/1 = ϕ[>1](z/1)z1/ 2 = ϕ[>1](z/1)z1/1 =z1/ 2),истинность которого и требуется доказать.Другими словами, надо показать, что формула A1A2A3B есть обще-значимая формула.Метод резолюций предназначен для доказательства противоречивости форму-лы. Таким образом, наша задача превращается в задачу доказательства того, чтоформула A1A2A3¬B невыполнима.Метод резолюций [4] как процедура опровержения применяется к «стандарт-ной форме» формулы и базируется на следующих принципах:Методика доказательства теорем для формальной системы ERM-модели 1191. Формула логики первого порядка может быть сведена к предваренной нор-мальной форме, в которой матрица не содержит никаких кванторов, а префиксесть последовательность кванторов.2. Поскольку матрица не содержит кванторов, она может быть сведена кконъюнктивной нормальной форме.3. Сохраняя противоречивость формулы, в ней можно элиминировать кванто-ры существования путем использования скулемовских функций.Пусть формула F находится в предваренной нормальной форме Q1x1...Qnxn(M) ,где М есть конъюнктивная нормальная форма. Положим, Qr есть квантор существо-вания в префиксе Q1x1...Qnxn ,1 ≤r≤n. Если никакой квантор всеобщности не сто-ит в префиксе левее Qr, мы выберем новую константу с, отличную от других кон-стант, входящих в М, заменим все xr, встречающиеся в М, на с и вычеркнем Qrxr изпрефикса. Если 1 ,..., Qs Qsm - список всех кванторов всеобщности, встречающихсялевее Qr, 1≤ s1 1](z/1))) .2. Перенести знак отрицания непосредственно к литерам, используя правилaa, законы де Моргана: ¬(ab)¬a¬b, ¬(ab)¬a¬b и формулыдля кванторов: ¬(x(F(x)))= x(¬F(x)) и ¬(x(F(x))) = x(¬F(x)) . В результа-те получается:z/1z1/1((¬z1/1 =ϕ[>1](z/1)y/1z2/1( y/1 =ϕ(z/1) y/1 =< z1/1, z2/1 >))(y/1z2/1(¬y/1 = ϕ(z/1)  ¬y/1 =) z1/1 = ϕ[> 1](z/1))) .3. Вынести кванторы в префикс формулы по соответствующим правилам:Qx(F(x))G = Qx(F(x)G),Qx(F(x))G=Qx(F(x)G),x(F(x)) x(G(x))= x(F(x)G(x)),x(F(x))  x(G(x)) = x(F(x) G(x)) ,Q1x(F(x)) Q2x(G(x))=Q1xQ2y(F(x)G(y)) ,Q1x(F(x))Q2x(G(x))=Q1xQ2y(F(x) G(y)) .Так как переменные y/1 и z2/1 встречаются два раза, в первом вхождении пере-именуем их в y/2 и z2/2 соответственно. Таким образом, после вынесения кванто-ров формула примет следующий вид:Методика доказательства теорем для формальной системы ERM-модели 121z/1z1/1y/2z2/2y/1z2/1((¬z1/1 =ϕ[>1](z/1)( y/ 2 =ϕ(z/1) y/ 2 =< z1/1, z2/ 2 >))(¬y/1 = ϕ(z/1)  ¬y/1 = z1/1 = ϕ[> 1](z/1))) .4. Привести матрицу формулы к конъюнктивной нормальной форме. Из [4]формула F находится в конъюнктивной нормальной форме, когда она представля-ет собой конъюнкцию формул F1, … Fn, где каждая из Fi есть дизъюнкция литер.Для приведения формулы к конъюнктивной нормальной форме используются ди-стрибутивные законы:a(bc)=(ab)(ac) иa(bc)=(ab)(ac).Конъюнктивная нормальная форма рассматриваемой формулы:z/1z1/1y/2z2/2y/1z2/1((¬z1/1 = ϕ[> 1](z/1)  y/ 2 = ϕ(z/1)) (¬z1/1 =ϕ[>1](z/1) y/ 2 =< z1/1,z2/ 2 >)(¬y/1 = ϕ(z/1)  ¬y/1 = z1/1 = ϕ[> 1](z/1))) .5. Привести формулу к скулемовской нормальной форме. Для каждого кванто-ра существования проверить все кванторы всеобщности, стоящие в префиксе ле-вее его. Если таковых нет, то переменная заменяется новой константой, иначе пе-ременная заменяется скулемовской функцией от всех переменных, связанныхэтими кванторами всеобщности:z/1z1/1y/1z2/1((¬z1/1 = ϕ[> 1](z/1)  f (z/1, z1/1) = ϕ(z/1)) (¬z1/1 = ϕ[>1](z/1) f(z/1,z1/1)=< z1/1,g(z/1,z1/1)>)(¬y/1 = ϕ(z/1)  ¬y/1 = z1/1 = ϕ[> 1](z/1))) .После приведения формулы к скулемовской нормальной форме отбрасывают-ся кванторы всеобщности и формула разбивается на дизъюнкты. Аксиома проек-ции породила три дизъюнкта:¬z1/1 = ϕ[>1](z/1) f(z/1,z1/1)= ϕ(z/1)¬z1/1 = ϕ[>1](z/1) f(z/1,z1/1)=< z1/1,g(z/1,z1/1)>¬y/1 =ϕ(z/1)¬y/1 =z1/1 =ϕ[>1](z/1).5. Формирование исходного множества дизъюнктов теоремыАлфавит формальной системы ТСЗО упрощает понимание выражений языкаи важен на этапе формулировки теорем и аксиом. Однако во время доказатель-ства можно заменить имена переменных на более простые. После приведениявсех формул к скулемовской нормальной форме и замены переменных (подста-новки указаны в фигурных скобках) для данной теоремы получим следующиедизъюнкты.122 А.М. Бабанов, А.С. СкачковаИз аксиомы проекции:{x/z/1,y1/z1/1}:¬y1 = ϕ[>1](x) f(x,y1) = ϕ(x),{x/z/1,y1/z1/1}:¬y1 = ϕ[>1](x) f(x,y1) = < y1,g(x,y1) > ,{x/z/1,y1 /z1/1,y/y/1,y2 /z2/1}:¬y= ϕ(x) ¬y= y1 = ϕ[>1](x) .Аксиома равенства сложных объектов породит 6 дизъюнктов, из которых длядоказательства понадобятся только 2:{x/y/1,x1/z1/1,x2 /z2/1,y/y/ 2,y1/z1/ 2,y2 /z2/ 2}:¬x =< x1,x2 > ¬y=< y1,y2 > ¬x= yx1= y1 и{x/y/1,x1/z1/1,x2 /z2/1,y/y/ 2,y1/z1/ 2,y2 /z2/ 2}:¬x =< x1,x2 > ¬y=< y1,y2 > ¬x= yx2 = y2.Из посылки:{x/z/1,y/y/1,z/y/ 2}:¬y= ϕ(x) ¬z= ϕ(x)y=z.Из отрицания заключения:{a/c1/1,c/c/1}:a= ϕ[>1](c),{b/c1/ 2,c/c/1}:b= ϕ[>1](c) ,{a/c1/1,b/c1/ 2}:¬a=b.Таким образом, получается список из 9 дизъюнктов теоремы:1. ¬y1= ϕ[>1](x) f(x,y1)= ϕ(x),2. ¬y1= ϕ[>1](x) f(x,y1)= < y1,g(x,y1)>,3. ¬y= ϕ(x) ¬y= y1= ϕ[>1](x),4. ¬x =< x1,x2 > ¬y=< y1,y2 > ¬x= yx1= y1,5. ¬x =< x1,x2 > ¬y=< y1,y2 > ¬x= yx2 = y2,6. ¬y=ϕ(x)¬z=ϕ(x)y=z,7. a= ϕ[>1](c),8. b= ϕ[>1](c),9. ¬a=b.6. Доказательство невыполнимости полученного множествадизъюнктов методом резолюцийТеперь методом резолюций докажем, что полученное множество дизъюнктовневыполнимо. Доказательство представляет собой последовательность порожде-ний резольвент для множества дизъюнктов. Каждая резольвента строится по пра-вилу резолюций [4].Для записи шагов доказательства используется следующий синтаксис:.(,) {}:.1. (1, 7) {a/y1,c/x}: f(c,a) = ϕ(c),2. (1, 8) {b/y1,c/x}: f(c,b) = ϕ(c),Методика доказательства теорем для формальной системы ERM-модели 1233. (6, 10) {f(c,a)/ y,c/x}:¬z = ϕ(c) f(c,a) = z ,4. (12, 11) {f(c,b)/z}: f(c,a)= f(c,b),5. (2, 7) {a/y1,c/x}: f(c,a) =,6. (2, 8) {b/y1,c/x}: f(c,b) =,7. (4, 13) {f (c,a)/ x, f (c,b)/ y}:¬f (c,a) =< x1,x2 > ¬f (c,b) =< y1, y2 > x1= y1,8. (16, 14) {a/x1,g(c,a)/x2}:¬f(c,b) =< y1,y2 > a= y1 ,9. (17, 15) {b/y1,g(c,b)/y2}:a=b,10. (18, 9) .Последним шагом доказательства получен пустой дизъюнкт, а, значит,наше исходное множество дизъюнктов невыполнимо. То есть формулаA1A2A3¬B противоречива, а, значит, формула A1A2A3B общезна-чима. Другими словами, наша теорема доказана.ЗаключениеПриведенная в статье методика доказательства теорем поможет исследовате-лям ERM-модели и ТСЗО развивать их формальную систему, что, в конечномсчете, послужит совершенствованию самих ERM-модели и ТСЗО.ЛИТЕРАТУРА1. Бабанов А.М. Развитие формальной системы теории семантически значимых отображе-ний // Вестник ТГУ. 2006. № 293. С. 135 - 139.2. Бабанов А.М. Семантическая модель «Сущность - Связь - Отображение» // ВестникТГУ. УВТиИ. 2007. № 1. С. 77 - 91.3. Бабанов А.М. Формальная система теории семантически значимых отображений // Вест-ник ТГУ. 2006. № 290. С. 261 - 263.4. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.:Наука, 1983. 360 с.Бабанов Алексей МихайловичСкачкова Анна СергеевнаТомский государственный университетE-mail: babanov@csd.tsu.ru; skachkova@indorsoft.ru Поступила в редакцию 1 февраля 2010 г

Скачать электронную версию публикации