Системы Theorema и автоматизация дедукции: сравнительный анализ

Рассмотрены основные парадигмы обработки математических знаний и обозначено место среди них систем Theorema и автоматизация дедукции. Описаны сравнительный анализ систем, общие черты их построения и различие в методах обработки данных. Basic paradigms of the mathematical knowledge processing are con...

Full description

Saved in:

Bibliographic Details
Published in:	Управляющие системы и машины
Date:	2011
Main Authors:	Анисимов, А.В., Джебелян, Т., Лялецкий, А.В., Попов, Н.
Format:	Article
Language:	Russian
Published:	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2011
Subjects:	Организационные и методические аспекты обеспечения непрерывного образования
Online Access:	https://nasplib.isofts.kiev.ua/handle/123456789/82950
Tags:	Add Tag No Tags, Be the first to tag this record!
Journal Title:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:	Системы Theorema и автоматизация дедукции: сравнительный анализ / А.В. Анисимов, Т. Джебелян, А.В. Лялецкий. Н. Попов // Управляющие системы и машины. — 2011. — № 4. — С. 59-63, 77. — Бібліогр.: 20 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

_version_	1860264579745972224
author	Анисимов, А.В. Джебелян, Т. Лялецкий, А.В. Попов, Н.
author_facet	Анисимов, А.В. Джебелян, Т. Лялецкий, А.В. Попов, Н.
citation_txt	Системы Theorema и автоматизация дедукции: сравнительный анализ / А.В. Анисимов, Т. Джебелян, А.В. Лялецкий. Н. Попов // Управляющие системы и машины. — 2011. — № 4. — С. 59-63, 77. — Бібліогр.: 20 назв. — рос.
collection	DSpace DC
container_title	Управляющие системы и машины
description	Рассмотрены основные парадигмы обработки математических знаний и обозначено место среди них систем Theorema и автоматизация дедукции. Описаны сравнительный анализ систем, общие черты их построения и различие в методах обработки данных. Basic paradigms of the mathematical knowledge processing are considered and the place of the Theorema and SAD systems is outlined. A comparative analysis of the systems, common features of their construction and the distinction in data processing methods are described. Розглянуто основні парадигми обробки математичних знань та позначено місце серед них систем Theorema та автоматизація дедукції. Описано порівняльний аналіз систем, загальні риси їх побудови та різницю в методах обробки даних.
first_indexed	2025-12-07T18:59:11Z
format	Article
fulltext	УСиМ, 2011, № 4 59 УДК 004.8:510.62:63 А.В. Анисимов, Т. Джебелян, А.В. Лялецкий. Н. Попов Системы Theorema и автоматизация дедукции: сравнительный анализ Рассмотрены основные парадигмы обработки математических знаний и обозначено место среди них систем Theorema и автоматиза- ция дедукции. Описаны сравнительный анализ систем, общие черты их построения и различие в методах обработки данных. Basic paradigms of the mathematical knowledge processing are considered and the place of the Theorema and SAD systems is outlined. A comparative analysis of the systems, common features of their construction and the distinction in data processing methods are described. Розглянуто основні парадигми обробки математичних знань та позначено місце серед них систем Theorema та автоматизація дедукції. Описано порівняльний аналіз систем, загальні риси їх побудови та різницю в методах обробки даних. Введение. В настоящее время повысилось вни- мание к созданию новых интеллектуальных сер- висов как на базе интеграции уже имеющихся информационных систем1, так и в результате создания новых компьютерных служб с исполь- зованием современных достижений в информа- тике и информационных технологиях. Это обусловлено тем, что решение задач автомати- зации интеллектуальной деятельности челове- ка требует умения компьютера проводить вы- числения и/или аналитические преобразова- ния, и/или логические рассуждения. Для дос- тижения этих целей имеется достаточно боль- шое количество различных служб, способных проводить числовые выкладки и/или символь- ные «вычисления», и/или дедуктивные построе- ния в среде формального естественного языка и успешно применяемых для решения разно- образных задач автоматизации рассуждений. Область автоматизации рассуждений пред- ставляет собой удачное сочетание теории и практики, хотя иногда оно оказывается иска- женно толкуемым. С одной стороны, специали- сты в прикладных вопросах центральной про- блемой считают эффективное применение име- ющихся теоретических результатов, но концен- трация внимания только на реализации часто вынуждает их оставлять без внимания те фун- даментальные проблемы, исследование кото- рых необходимо для решения задач. С другой стороны, специалисты в фундаментальных во- просах обращают основное внимание на внут- реннее теоретическое развитие своих исследо- ваний, акцентируя его на решении сложных 1 Такие системы в дальнейшем называются компьютер- ными математическими службами или просто службами. проблем. Вопросы же реализации трактуются ими как «чисто прагматические», «инженер- ные» задачи. Поэтому естественно стремиться к нахождению разумного баланса между этими двумя точками зрения, одновременно развивая в автоматизации рассуждений те теоретиче- ские и прикладные стороны математической логики, символьных преобразований и лин- гвистики, которые могут привести к эффек- тивной реализации на компьютерах соответст- вующих подходов, методов и средств. Именно с этих позиций проводились разработка и реа- лизация систем Theorema и автоматизация де- дукции (САД). Разработка и реализация системы Theorema [1] началась во второй половине 1990-х гг. в соответствии с одноименной программой [2]. Приблизительно в то же время были возобнов- лены работы по САД в англоязычной версии2 [3] в рамках работ по реализации программы Алгоритм Очевидности [4]. Обе эти системы с самого начала их разработки были ориентиро- ваны на оказание разнообразной помощи чело- веку в его математической деятельности. Да- дим более детальное их описание и проведем сравнение систем в рамках существующих па- радигм автоматизации рассуждений и стилей обработки математических знаний. Парадигмы обработки компьютерных зна- ний и системы Theorema и САД На современном этапе можно выделить сле- дующие парадигмы обработки компьютерных математических знаний. 2 Русскоязычная версия САД [5] была разработана и реализована во второй половине 1970-х гг. в рамках ра- бот по программе Алгоритм Очевидности. 60 УСиМ, 2011, № 4 Числовая парадигма отображает методы и средства приближенного или точного решения задач чистой или прикладной математики, что основывается на построении конечной после- довательности действий над конечным множе- ством чисел. Обычно ее использование начи- нается с построения математической (контину- альной) модели. После этого совершается пе- реход к ее дискретному представлению, что позволяет разрабатывать различные алгоритмы числовых вычислений, которые впоследствии программируются на компьютерах в виде па- кетов прикладных программ. Символьная (аналитическая) парадигма ба- зируется на возможности компьютера выпол- нять сложные символьные преобразования и числовые выкладки, строить графики функций, задавать модели необходимых процессов и др. Она ориентирована на построение и использо- вание так называемых систем компьютерной алгебры (СКА) и возникла во второй половине 1960-х годов как альтернатива числовой пара- дигме в связи с появлением компьютеров та- кой скорости, информационной емкости и гиб- кости, что стало возможным программирова- ние сложных интеллектуальных процессов. По- явление СКА было вызвано также следующи- ми обстоятельствами:  наличием задач, которые не могут быть легко выполнены человеком при помощи руч- ки и листа бумаги, и для которых практически отсутствуют их адекватные представления в виде соответствующих числовых алгоритмов;  уменьшением затрат времени и усилий на нахождение решения широкого круга научно- прикладных задач;  компактностью записи и наглядностью ана- литического решения поставленной задачи в сравнении с ее числовым решением. Принципы построения СКА хорошо согла- суются с эмпирическим опытом человека, при- обретенным при решении различных матема- тических и естественнонаучных задач. В то же время в современных СКА, как правило, пол- ностью отсутствуют средства проведения ло- гических рассуждений. Дедуктивная парадигма использует тот факт, что существующие в компьютере знания име- ют вид определенных синтаксических единиц (как правило, аксиом, определений, утвержде- ний, теорем и пр.), а дополнительные знания по- лучаются из имеющихся посредством приме- нения к ним определенных схем умозаключе- ний. Системы представления и обработки зна- ний, основанные на этой парадигме, получили название систем автоматизации рассуждений, значительная часть которых существует в виде систем доказательства теорем, поскольку имен- но логико-математический подход наиболее ре- левантен и эффективен при решении задач на построение цепочек дедуктивных рассуждений во многих прикладных областях (различаются декларативные и интерактивные системы ав- томатизации рассуждений). Для того чтобы некоторая система автома- тизации рассуждений могла оказывать дедуктив- ную помощь человеку, очевидно, что необходи- мо разработать подходящую языковую «обо- лочку», правильно сформулировать аксиомы и правила порождения новых утверждений из уже имеющихся, уметь генерировать предпо- ложения и гипотезы, которыми можно пользо- ваться, и пр.1 Интеграционная парадигма. Можно выде- лить два основных типа системной интегра- ции: интеграцию на этапе проектирования, ко- гда еще во время разработки системы преду- сматривается как наличие в ней компьютерных служб разного рода, так и возможность ее ие- рархического наращивания путем подключе- ния к ней имеющихся служб (солверов, СКА и др.) и интеграцию на этапе эксплуатации, ко- гда осуществляется предопределенное задачей комбинирование в одну систему готовых ком- пьютерных служб (особое внимание к разра- ботке систем такого типа вызвало появление информационных технологий, основанных на широком использовании сети Интернет). 1 Конечно, в контексте данной работы в качестве альтер- нативы дедуктивной парадигме следует упомянуть индук- тивную парадигму, которая охватывает процессы рассуж- дений, основанные на переходе от частных положений к некоторым гипотезам/общим утверждениям. (Такой спо- соб рассуждений пока не нашел своего отражения в имею- щихся версиях системы Theorema и САД). УСиМ, 2011, № 4 61 Если теперь обратиться к системе Theorema и САД, то они могут рассматриваться как яр- кие представители интеграционной парадигмы первого типа (например, [6, 7]). Остановимся на этом подробнее. Как упоминалось, система Theorema появи- лась в результате попытки реализации одно- именного проекта, ориентированного в перво- начальной постановке на создание декларатив- ной логической надстройки [8] над известным пакетом компьютерной алгебры Mathematiсa [9]1, что позволило позднее сориентировать ее на изучение математических теорий [10]. САД с самого начала задумывалась как дек- ларативная дедуктивная система, предназна- ченная для оказания помощи математику в его научной деятельности. В ходе разработки САД ее архитектура проектировалась так, чтобы было возможно подключение различных мате- матических служб, включая системы компью- терной алгебры и пруверы [12]. Опишем некоторые особенности и возмож- ности системы Theorema и САД, сравнивая ос- новные принципы их построения. Система Theorema и САД в качестве своих входных языков используют формальные язы- ки естественного типа, основное различие ме- жду которыми состоит в том, что входной язык САД представляет собой формальный естест- венный язык, который может быть транслиру- ем в обычный язык логики предикатов первого порядка, в то время как входной язык Theo- rema есть естественная разновидность языка логики высших порядков. Кроме того, Theo- rema включает в себя простой и удобный про- цедурный язык, обеспечивающий возможность проведения числовых вычислений и символь- ных преобразований в «контексте» логических рассуждений. Выбор языков для системы Theorema и САД объясняет и различие в выборе их логических аппаратов: Theorema использует методы поис- ка вывода в логике высших порядков, а САД – 1 Позже Theorema начала развиваться и в других на- правлениях, например, использоваться для верификации программного обеспечения [11]. в классической логике первого порядка. Обе системы также оснащены и машинно-ориенти- рованными эвристическими приемами доказа- тельств, конечно, учитывающими логики, с ко- торыми они работают. Дополнительно можно еще отметить, что собственный логический ап- парат САД развивался так, чтобы можно было проводить поиск логического вывода в сигна- туре исходной теории с возможностью отделе- ния обработки равенств от процесса дедукции для возможного использования внешних (по отношению к САД) солверов, в частности, сис- тем компьютерной алгебры. Для завершения описания принципов постро- ения и сравнения системы Theorema и САД зафиксируем более четко их место среди пере- численных парадигм обработки математиче- ских знаний. Прежде всего, обратим внимание на то, что в силу отмеченных языковых особенностей как Theorema, так и САД относятся к дедуктивной парадигме, базирующейся на декларативном подходе. Но при этом они используют разные логические аппараты. Что же касается остальных парадигм, то на- личие в системе Theorema средств процедур- ного программирования допускает реализацию на компьютере разных вычислительных алго- ритмов, а возможность привлечения к ее рабо- те системы Mathematica позволяет говорить, что Theorema использует не только вычислитель- ную, но и символьную парадигму. В системе же САД отсутствуют средства программирования в рамках вычислительной и символьных парадигм. Она спроектирована на принципе привлечения извне компьютерных служб, представляющих эти парадигмы, с уче- том ее архитектуры и хорошо развитых языко- вых средств, дающих возможность интеграции различных подходов к обработке знаний. Стили обработки данных в системе Theo- rema и САД Целесообразно также сравнить систему Theo- rema и САД относительно стилей представле- ния и обработки данных при решении задач автоматизации рассуждений, к наиболее инте- ресным из которых принадлежат стиль прове- 62 УСиМ, 2011, № 4 дения доказательств, степень подробности до- казательств и стиль формализации. Стиль проведения доказательства. Суще- ственным свойством систем оказания помощи в автоматизации рассуждений есть вид их вход- ных данных. Так называемые интерактивные системы (первой тип) чаще всего тактико-уп- равляемы, а это значит, что заданное утверж- дение доказывается с помощью последователь- ности инструкций, вводимых в систему. Эти ин- струкции (т.е. тактики) могут быть примитив- ными, представляющими собой однократное применение правила вывода, или более слож- ными, подобными плану доказательства или привлечению к обработке рассматриваемой це- ли некоторого внешнего (по отношению к сис- теме) прувера. К системам такого типа относятся Isabelle [14], Coq [15], HOL [16] и др. Работа с такими системами удобна и легка в случае, ко- гда она предоставляет в распоряжение пользо- вателя изящный набор мощных тактик, доста- точных для решения задачи. Второй тип систем ориентирован на декла- ративное представление решаемой задачи, от- ражающее стиль обычных математических пуб- ликаций, когда доказываемые утверждения и, при необходимости, их доказательства записы- ваются на некотором формальном языке, кото- рый должен быть расширяем средствами (логи- ческого) структурирования текста. Верифици- рующая система такого рода должна обладать способностью проверки правильности каждого шага доказательства, т.е. она должна управлять- ся доказательством (при наличии такового). Наиболее типичными образцами этого под- хода для классической логики первого порядка есть САД и система Mizar [17] , в то время как для логики высших порядков декларативный стиль наиболее отслежен в системе Theorema. Заметим, что система Isabelle, расширенная средствами Isar [18] вместе с языком для запи- си структурированных доказательств, имитиру- ющий стиль математических рассуждений, так- же может служить представителем систем, уп- равляемых задаваемым доказательством. Приведенное различие между двумя типами входных данных не очень существенно. Если можно построить доказательства теорем с по- мощью тактико-управляемой системой, ис- пользующей промежуточный ввод целей и ав- томатическое закрытие подцелей, то такая сис- тема может рассматриваться как управляемая доказательством. Обратно, если шаги вывода, воспринимаемого некоторой системой, управ- ляемой доказательством, снабжены детальны- ми подсказками о приемах и методах верифи- кации, то такая система может рассматривать- ся как тактико-управляемая. Степень «грануляции». Дедуктивная мощь систем поддержки автоматизации рассуждений может меняться в зависимости от требований, выставляемых пользователем. Поэтому можно считать, что название таких систем колеблется между системами верификации доказательств и системами поиска доказательств. Первые при- нимают на вход только шаги доказательства, имеющие вид применений правил вывода, и, следовательно, должны быть детализированы с точностью до правил вывода. Система Mizar служит примером такой системы, хотя набор ее правил вывода достаточно велик. Системы, относящиеся к системам поиска доказательств и/или верификации текстов, со- держат методы поиска вывода и/или плани- ровщики доказательств и пытаются воспол- нить «недостающие» места доказательства, используя «зашитую» логику (логики). Систе- мы САД и Theorema, а также Nqthm [19] и ACL2 [20] – характерные представители сис- тем такого рода. Тактико-управляемые системы типа Isabelle и Coq обычно обладают исчерпывающими (для проведения доказательств) наборами тактик, так что их «дедуктивная мощь» может не иметь принципиального значения. И в этой связи они могут рассматриваться как системы построе- ния доказательств. Однако некоторые экспе- рименты с Isabelle и Coq показывают, что сле- дующая ситуация может оказаться критиче- ской для них: при всякой попытке «сразу же» доказать теорему «диалог» о построении дока- зательства становится сложным, сильно вет- вящимся и тяжело отслеживаемым без предва- рительного выделения лемм, без применения УСиМ, 2011, № 4 63 специальных тактик и использования суще- ствующих библиотек. Стиль формализации. На стиль формали- зации обрабатываемого текста оказывают вли- яние предметная область, предварительные све- дения, вид применяемых определений (явля- ются ли они «компьютеризируемыми»), спо- соб рассуждения (является ли он конструктив- ным, строго типизируемым или основанным на том или ином исчислении) и др. Также на стиль формализации влияют используемая базовая ло- гика и теории, вовлекаемые в формализацию. Существует два основных стиля формали- зации: первый ориентирован на применение логик высших порядков (с теорией типов в ка- честве математической базы), а второй – на логику первого порядка (как правило, с теори- ей множеств в качестве математической базы). В силу изложенного, система Theorema от- носится к первому стилю формализации. Заме- тим, что теоретико-типовой подход применя- ется в большинстве хорошо известных систем, оказывающих математическую помощь таких, как Isabelle, Coq, HOL и др. При этом предпоч- тение его использованию, как правило, отдает- ся в случаях обращения к индуктивно-опреде- ляемым областям и рекурсивным определени- ям. Он также хорошо подходит к формализации программистских и инженерных концепций. К примерам второго стиля относится САД и упомянутая система Mizar, использующая логи- ку первого порядка и теорию множеств Тарско- го–Гротендика. Такая ориентация Mizar соот- ветствует традиционному способу построения математики; существует больший набор матема- тических утверждений, проверенных в Mizar. В отличие от Mizar система САД не адапти- рована к какой-нибудь теории множеств (или другой фундаментальной теории), дающей об- щую основу для формализации. Вместо этого, для решения задачи пользователю предлагает- ся задать необходимый набор предварительных сведений, выражающих базовые концепции на естественном формальном языке, транслируе- мом в определенную разновидность языка пер- вого порядка; также требуется указать логиче- ский прувер, наиболее релевантный для нахо- ждения искомого решения. Заключение. Итак, Theorema и САД базиру- ются на идейно близких платформах, есть пред- ставителями интеграционной парадигмы с де- кларативным представлением знаний и обла- дают рядом как общих, так и различных прин- ципов построения и стилей символьной и ло- гической обработки данных. Это делает при- влекательными попытки, которые могут быть совершены в направлении совершенствования САД путем применения оригинальных идей и опыта, полученного разработчиками системы Theorema в ходе ее имплементации и эксплуа- тации, и наоборот. В долгосрочной перспективе исследования по дальнейшему развитию системы Theorema и САД, их развитию и взаимному обогащению могут привести к созданию мощной инфра- структуры по оказанию помощи как в проведе- нии научных исследований, так и в образова- нии. Они могут оказаться полезными при ре- шении задач верификации, а также при созда- нии систем управления компьютерными зна- ниями. 1. Buchberger B., Jebelean T. Theorema: The predicate logic prover // Proc. of the First Intern. Theorema Workshop. – Hagenberg, Austria, 1997. 2. A Survey of the Theorema project / B. Buchberger, T. Je- belean, F. Kriftner et al. // Proc. of the Intern. Symp. on Symb. and Algebr. Comp. (ISSAC'97). – 1997. – P. 384–391. 3. System for Automated Deduction (SAD): Linguistic and deductive peculiarities / A. Degtyarev, A. Lyaletski, K. Verchinine et al. // Proc. of the 11th Intern. Symp. IIS 2002. – Poland, 2002. – P. 413–422. 4. Глушков В.М. Некоторые проблемы теории автома- тов и искусственного интеллекта // Кибернетика. – 1970. – № 2. – С. 3–13. 5. О системе обработки математических текстов / Ю.В. Капитонова, К.П. Вершинин, А.И. Дегтярев и др. // Там же. – 1979. – № 2. – С. 48–55. 6. Theorema: An integrated system for computation and deduction in natural style / B. Buchberger, K. Aigner, C. Dupre et al. // RISC Report Series, Johannes Kepler Univ. of Linz, Austria. – 1998. 7. Lyaletski A., Verchinine K., Paskevich A. Theorem proving and proof verification in the system SAD // Lecture Notes in Computer Science (Proc. of the 3rd Intern. Conf. MKM 2004). – 2004. – 3119. – P. 236–250. Окончание на стр. 77 УСиМ, 2011, № 4 77 Окончание статьи А.В. Анисимова и др. 8. Buchberger B. Theorema: A proving system based on Mathematica // The Mathematica J. – 2001. – 8(2). – P. 247–252. 9. The Mathematica Book. – http://reference.wolfram.com/ legacy/v5/ TheMathematicaBook/index.html 10. Theorema: Towards Computer-Aided Mathematical The- ory Exploration / B. Buchberger, A. Craciun, T. Jebelean et al. // J. of Applied Logic. – 2006. – 4(4). – P. 470–504. 11. Kovacs L., Popov N., Jebelean T. Combining Logic and Algebraic Techniques for Program Verification in Theo- rema // Proc. of Second Intern. Symp. on Leveraging Appl. of Formal Methods, Verification and Validation (ISOLA 2006). – Paphos, Cyprus, 2006. – P. 59–68. 12. Anisimov А., Lyaletski А. The SAD system in three di- mensions // Proc. of the 7th Intern. Workshop on Symb. and Numeric Algorithms for Scientific Comp. (SYNASC 2006). – Timisoara, Romania, 2006. – P. 85–88. 13. Анисимов А.В., Джебелян Т., Лялецкий А.В., Попов Н. Проекты Алгоритм Очевидности и Theorema: их осо- бенности и реализация на современном этапе // Тез. доп. Міжнар. конф. TAAPSD 2010. – Київ, Україна, 2010. – С. 54–58. 14. The Isabell. – http://www.cl.cam.ac.uk/Research/HVG/ Isabelle/ 15. The Coq system. – http://coq.inria.fr/ 16. The system HOL. – http://www.cl.cam.ac.uk/Research/ HVG/HOL/ 17. The Mizar System. – http://mizar.uwb.edu.pl/ 18. The Isar site. – http://isabelle.in.tum.de/Isar/ 19. The Ngth system. – http://www.cli.com/software/nqthm/ 20. The ACL2 System. – http://www.cs.utexas.edu/users/ moore/acl2/ © А.В. Анисимов, Т. Джебелян, А.В. Лялецкий. Н. Попов, 2011  9.pdf 77.pdf << /ASCII85EncodePages false /AllowTransparency false /AutoPositionEPSFiles true /AutoRotatePages /None /Binding /Left /CalGrayProfile (Dot Gain 20%) /CalRGBProfile (sRGB IEC61966-2.1) /CalCMYKProfile (U.S. Web Coated \050SWOP\051 v2) /sRGBProfile (sRGB IEC61966-2.1) /CannotEmbedFontPolicy /Error /CompatibilityLevel 1.4 /CompressObjects /Tags /CompressPages true /ConvertImagesToIndexed true /PassThroughJPEGImages true /CreateJobTicket false /DefaultRenderingIntent /Default /DetectBlends true /DetectCurves 0.0000 /ColorConversionStrategy /CMYK /DoThumbnails false /EmbedAllFonts true /EmbedOpenType false /ParseICCProfilesInComments true /EmbedJobOptions true /DSCReportingLevel 0 /EmitDSCWarnings false /EndPage -1 /ImageMemory 1048576 /LockDistillerParams false /MaxSubsetPct 100 /Optimize true /OPM 1 /ParseDSCComments true /ParseDSCCommentsForDocInfo true /PreserveCopyPage true /PreserveDICMYKValues true /PreserveEPSInfo true /PreserveFlatness true /PreserveHalftoneInfo false /PreserveOPIComments true /PreserveOverprintSettings true /StartPage 1 /SubsetFonts true /TransferFunctionInfo /Apply /UCRandBGInfo /Preserve /UsePrologue false /ColorSettingsFile () /AlwaysEmbed [ true ] /NeverEmbed [ true ] /AntiAliasColorImages false /CropColorImages true /ColorImageMinResolution 300 /ColorImageMinResolutionPolicy /OK /DownsampleColorImages true /ColorImageDownsampleType /Bicubic /ColorImageResolution 300 /ColorImageDepth -1 /ColorImageMinDownsampleDepth 1 /ColorImageDownsampleThreshold 1.50000 /EncodeColorImages true /ColorImageFilter /DCTEncode /AutoFilterColorImages true /ColorImageAutoFilterStrategy /JPEG /ColorACSImageDict << /QFactor 0.15 /HSamples [1 1 1 1] /VSamples [1 1 1 1] >> /ColorImageDict << /QFactor 0.15 /HSamples [1 1 1 1] /VSamples [1 1 1 1] >> /JPEG2000ColorACSImageDict << /TileWidth 256 /TileHeight 256 /Quality 30 >> /JPEG2000ColorImageDict << /TileWidth 256 /TileHeight 256 /Quality 30 >> /AntiAliasGrayImages false /CropGrayImages true /GrayImageMinResolution 300 /GrayImageMinResolutionPolicy /OK /DownsampleGrayImages true /GrayImageDownsampleType /Bicubic /GrayImageResolution 300 /GrayImageDepth -1 /GrayImageMinDownsampleDepth 2 /GrayImageDownsampleThreshold 1.50000 /EncodeGrayImages true /GrayImageFilter /DCTEncode /AutoFilterGrayImages true /GrayImageAutoFilterStrategy /JPEG /GrayACSImageDict << /QFactor 0.15 /HSamples [1 1 1 1] /VSamples [1 1 1 1] >> /GrayImageDict << /QFactor 0.15 /HSamples [1 1 1 1] /VSamples [1 1 1 1] >> /JPEG2000GrayACSImageDict << /TileWidth 256 /TileHeight 256 /Quality 30 >> /JPEG2000GrayImageDict << /TileWidth 256 /TileHeight 256 /Quality 30 >> /AntiAliasMonoImages false /CropMonoImages true /MonoImageMinResolution 1200 /MonoImageMinResolutionPolicy /OK /DownsampleMonoImages true /MonoImageDownsampleType /Bicubic /MonoImageResolution 1200 /MonoImageDepth -1 /MonoImageDownsampleThreshold 1.50000 /EncodeMonoImages true /MonoImageFilter /CCITTFaxEncode /MonoImageDict << /K -1 >> /AllowPSXObjects false /CheckCompliance [ /None ] /PDFX1aCheck false /PDFX3Check false /PDFXCompliantPDFOnly false /PDFXNoTrimBoxError true /PDFXTrimBoxToMediaBoxOffset [ 0.00000 0.00000 0.00000 0.00000 ] /PDFXSetBleedBoxToMediaBox true /PDFXBleedBoxToTrimBoxOffset [ 0.00000 0.00000 0.00000 0.00000 ] /PDFXOutputIntentProfile () /PDFXOutputConditionIdentifier () /PDFXOutputCondition () /PDFXRegistryName () /PDFXTrapped /False /CreateJDFFile false /Description << /ARA <FEFF06270633062A062E062F0645002006470630064700200627064406250639062F0627062F0627062A002006440625064606340627062100200648062B062706260642002000410064006F00620065002000500044004600200645062A064806270641064206290020064406440637062806270639062900200641064A00200627064406450637062706280639002006300627062A0020062F0631062C0627062A002006270644062C0648062F0629002006270644063906270644064A0629061B0020064A06450643064600200641062A062D00200648062B0627062606420020005000440046002006270644064506460634062306290020062806270633062A062E062F062706450020004100630072006F0062006100740020064800410064006F006200650020005200650061006400650072002006250635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E0635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E> /BGR <FEFF04180437043f043e043b043704320430043904420435002004420435043704380020043d0430044104420440043e0439043a0438002c00200437043000200434043000200441044a0437043404300432043004420435002000410064006f00620065002000500044004600200434043e043a0443043c0435043d04420438002c0020043c0430043a04410438043c0430043b043d043e0020043f044004380433043e04340435043d04380020043704300020043204380441043e043a043e043a0430044704350441044204320435043d0020043f04350447043004420020043704300020043f044004350434043f0435044704300442043d04300020043f043e04340433043e0442043e0432043a0430002e002000200421044a04370434043004340435043d043804420435002000500044004600200434043e043a0443043c0435043d044204380020043c043e0433043004420020043404300020044104350020043e0442043204300440044f0442002004410020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200441043b0435043404320430044904380020043204350440044104380438002e> /CHS <FEFF4f7f75288fd94e9b8bbe5b9a521b5efa7684002000410064006f006200650020005000440046002065876863900275284e8e9ad88d2891cf76845370524d53705237300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c676562535f00521b5efa768400200050004400460020658768633002> /CHT <FEFF4f7f752890194e9b8a2d7f6e5efa7acb7684002000410064006f006200650020005000440046002065874ef69069752865bc9ad854c18cea76845370524d5370523786557406300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c4f86958b555f5df25efa7acb76840020005000440046002065874ef63002> /CZE <FEFF005400610074006f0020006e006100730074006100760065006e00ed00200070006f0075017e0069006a007400650020006b0020007600790074007600e101590065006e00ed00200064006f006b0075006d0065006e0074016f002000410064006f006200650020005000440046002c0020006b00740065007200e90020007300650020006e0065006a006c00e90070006500200068006f006400ed002000700072006f0020006b00760061006c00690074006e00ed0020007400690073006b00200061002000700072006500700072006500730073002e002000200056007900740076006f01590065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f007400650076015900ed007400200076002000700072006f006700720061006d0065006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076011b006a016100ed00630068002e> /DAN <FEFF004200720075006700200069006e0064007300740069006c006c0069006e006700650072006e0065002000740069006c0020006100740020006f007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400650072002c0020006400650072002000620065006400730074002000650067006e006500720020007300690067002000740069006c002000700072006500700072006500730073002d007500640073006b007200690076006e0069006e00670020006100660020006800f8006a0020006b00760061006c0069007400650074002e0020004400650020006f007000720065007400740065006400650020005000440046002d0064006f006b0075006d0065006e0074006500720020006b0061006e002000e50062006e00650073002000690020004100630072006f00620061007400200065006c006c006500720020004100630072006f006200610074002000520065006100640065007200200035002e00300020006f00670020006e0079006500720065002e> /DEU <FEFF00560065007200770065006e00640065006e0020005300690065002000640069006500730065002000450069006e007300740065006c006c0075006e00670065006e0020007a0075006d002000450072007300740065006c006c0065006e00200076006f006e002000410064006f006200650020005000440046002d0044006f006b0075006d0065006e00740065006e002c00200076006f006e002000640065006e0065006e002000530069006500200068006f006300680077006500720074006900670065002000500072006500700072006500730073002d0044007200750063006b0065002000650072007a0065007500670065006e0020006d00f60063006800740065006e002e002000450072007300740065006c006c007400650020005000440046002d0044006f006b0075006d0065006e007400650020006b00f6006e006e0065006e0020006d006900740020004100630072006f00620061007400200075006e0064002000410064006f00620065002000520065006100640065007200200035002e00300020006f0064006500720020006800f600680065007200200067006500f600660066006e00650074002000770065007200640065006e002e> /ESP <FEFF005500740069006c0069006300650020006500730074006100200063006f006e0066006900670075007200610063006900f3006e0020007000610072006100200063007200650061007200200064006f00630075006d0065006e0074006f00730020005000440046002000640065002000410064006f0062006500200061006400650063007500610064006f00730020007000610072006100200069006d0070007200650073006900f3006e0020007000720065002d0065006400690074006f007200690061006c00200064006500200061006c00740061002000630061006c0069006400610064002e002000530065002000700075006500640065006e00200061006200720069007200200064006f00630075006d0065006e0074006f00730020005000440046002000630072006500610064006f007300200063006f006e0020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e003000200079002000760065007200730069006f006e0065007300200070006f00730074006500720069006f007200650073002e> /ETI <FEFF004b00610073007500740061006700650020006e0065006900640020007300e4007400740065006900640020006b00760061006c006900740065006500740073006500200074007200fc006b006900650065006c007300650020007000720069006e00740069006d0069007300650020006a0061006f006b007300200073006f00620069006c0069006b0065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740069006400650020006c006f006f006d006900730065006b0073002e00200020004c006f006f0064007500640020005000440046002d0064006f006b0075006d0065006e00740065002000730061006100740065002000610076006100640061002000700072006f006700720061006d006d006900640065006700610020004100630072006f0062006100740020006e0069006e0067002000410064006f00620065002000520065006100640065007200200035002e00300020006a00610020007500750065006d006100740065002000760065007200730069006f006f006e00690064006500670061002e000d000a> /FRA <FEFF005500740069006c006900730065007a00200063006500730020006f007000740069006f006e00730020006100660069006e00200064006500200063007200e900650072002000640065007300200064006f00630075006d0065006e00740073002000410064006f00620065002000500044004600200070006f0075007200200075006e00650020007100750061006c0069007400e90020006400270069006d007000720065007300730069006f006e00200070007200e9007000720065007300730065002e0020004c0065007300200064006f00630075006d0065006e00740073002000500044004600200063007200e900e90073002000700065007500760065006e0074002000ea0074007200650020006f007500760065007200740073002000640061006e00730020004100630072006f006200610074002c002000610069006e00730069002000710075002700410064006f00620065002000520065006100640065007200200035002e0030002000650074002000760065007200730069006f006e007300200075006c007400e90072006900650075007200650073002e> /GRE <FEFF03a703c103b703c303b903bc03bf03c003bf03b903ae03c303c403b5002003b103c503c403ad03c2002003c403b903c2002003c103c503b803bc03af03c303b503b903c2002003b303b903b1002003bd03b1002003b403b703bc03b903bf03c503c103b303ae03c303b503c403b5002003ad03b303b303c103b103c603b1002000410064006f006200650020005000440046002003c003bf03c5002003b503af03bd03b103b9002003ba03b103c42019002003b503be03bf03c703ae03bd002003ba03b103c403ac03bb03bb03b703bb03b1002003b303b903b1002003c003c103bf002d03b503ba03c403c503c003c903c403b903ba03ad03c2002003b503c103b303b103c303af03b503c2002003c503c803b703bb03ae03c2002003c003bf03b903cc03c403b703c403b103c2002e0020002003a403b10020005000440046002003ad03b303b303c103b103c603b1002003c003bf03c5002003ad03c703b503c403b5002003b403b703bc03b903bf03c503c103b303ae03c303b503b9002003bc03c003bf03c103bf03cd03bd002003bd03b1002003b103bd03bf03b903c703c403bf03cd03bd002003bc03b5002003c403bf0020004100630072006f006200610074002c002003c403bf002000410064006f00620065002000520065006100640065007200200035002e0030002003ba03b103b9002003bc03b503c403b103b303b503bd03ad03c303c403b503c103b503c2002003b503ba03b403cc03c303b503b903c2002e> /HEB <FEFF05D405E905EA05DE05E905D5002005D105D405D205D305E805D505EA002005D005DC05D4002005DB05D305D9002005DC05D905E605D505E8002005DE05E105DE05DB05D9002000410064006F006200650020005000440046002005D405DE05D505EA05D005DE05D905DD002005DC05D405D305E405E105EA002005E705D305DD002D05D305E405D505E1002005D005D905DB05D505EA05D905EA002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E05D005DE05D905DD002005DC002D005000440046002F0058002D0033002C002005E205D905D905E005D5002005D105DE05D305E805D905DA002005DC05DE05E905EA05DE05E9002005E905DC0020004100630072006F006200610074002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E> /HRV (Za stvaranje Adobe PDF dokumenata najpogodnijih za visokokvalitetni ispis prije tiskanja koristite ove postavke. Stvoreni PDF dokumenti mogu se otvoriti Acrobat i Adobe Reader 5.0 i kasnijim verzijama.) /HUN <FEFF004b0069007600e1006c00f30020006d0069006e0151007300e9006701710020006e0079006f006d00640061006900200065006c0151006b00e90073007a00ed007401510020006e0079006f006d00740061007400e100730068006f007a0020006c006500670069006e006b00e1006200620020006d0065006700660065006c0065006c0151002000410064006f00620065002000500044004600200064006f006b0075006d0065006e00740075006d006f006b0061007400200065007a0065006b006b0065006c0020006100200062006500e1006c006c00ed007400e10073006f006b006b0061006c0020006b00e90073007a00ed0074006800650074002e0020002000410020006c00e90074007200650068006f007a006f00740074002000500044004600200064006f006b0075006d0065006e00740075006d006f006b00200061007a0020004100630072006f006200610074002000e9007300200061007a002000410064006f00620065002000520065006100640065007200200035002e0030002c0020007600610067007900200061007a002000610074007400f3006c0020006b00e9007301510062006200690020007600650072007a006900f3006b006b0061006c0020006e00790069007400680061007400f3006b0020006d00650067002e> /ITA <FEFF005500740069006c0069007a007a006100720065002000710075006500730074006500200069006d0070006f007300740061007a0069006f006e00690020007000650072002000630072006500610072006500200064006f00630075006d0065006e00740069002000410064006f00620065002000500044004600200070006900f900200061006400610074007400690020006100200075006e00610020007000720065007300740061006d0070006100200064006900200061006c007400610020007100750061006c0069007400e0002e0020004900200064006f00630075006d0065006e007400690020005000440046002000630072006500610074006900200070006f00730073006f006e006f0020006500730073006500720065002000610070006500720074006900200063006f006e0020004100630072006f00620061007400200065002000410064006f00620065002000520065006100640065007200200035002e003000200065002000760065007200730069006f006e006900200073007500630063006500730073006900760065002e> /JPN <FEFF9ad854c18cea306a30d730ea30d730ec30b951fa529b7528002000410064006f0062006500200050004400460020658766f8306e4f5c6210306b4f7f75283057307e305930023053306e8a2d5b9a30674f5c62103055308c305f0020005000440046002030d530a130a430eb306f3001004100630072006f0062006100740020304a30883073002000410064006f00620065002000520065006100640065007200200035002e003000204ee5964d3067958b304f30533068304c3067304d307e305930023053306e8a2d5b9a306b306f30d530a930f330c8306e57cb30818fbc307f304c5fc59808306730593002> /KOR <FEFFc7740020c124c815c7440020c0acc6a9d558c5ec0020ace0d488c9c80020c2dcd5d80020c778c1c4c5d00020ac00c7a50020c801d569d55c002000410064006f0062006500200050004400460020bb38c11cb97c0020c791c131d569b2c8b2e4002e0020c774b807ac8c0020c791c131b41c00200050004400460020bb38c11cb2940020004100630072006f0062006100740020bc0f002000410064006f00620065002000520065006100640065007200200035002e00300020c774c0c1c5d0c11c0020c5f40020c2180020c788c2b5b2c8b2e4002e> /LTH <FEFF004e006100750064006f006b0069007400650020016100690075006f007300200070006100720061006d006500740072007500730020006e006f0072011700640061006d00690020006b0075007200740069002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b00750072006900650020006c0061006200690061007500730069006100690020007000720069007400610069006b007900740069002000610075006b01610074006f00730020006b006f006b007900620117007300200070006100720065006e006700740069006e00690061006d00200073007000610075007300640069006e0069006d00750069002e0020002000530075006b0075007200740069002000500044004600200064006f006b0075006d0065006e007400610069002000670061006c006900200062016b007400690020006100740069006400610072006f006d00690020004100630072006f006200610074002000690072002000410064006f00620065002000520065006100640065007200200035002e0030002000610072002000760117006c00650073006e0117006d00690073002000760065007200730069006a006f006d00690073002e> /LVI <FEFF0049007a006d0061006e0074006f006a00690065007400200161006f00730020006900650073007400610074012b006a0075006d00750073002c0020006c0061006900200076006500690064006f00740075002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006100730020006900720020012b00700061016100690020007000690065006d01130072006f00740069002000610075006700730074006100730020006b00760061006c0069007401010074006500730020007000690072006d007300690065007300700069006501610061006e006100730020006400720075006b00610069002e00200049007a0076006500690064006f006a006900650074002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006f002000760061007200200061007400760113007200740020006100720020004100630072006f00620061007400200075006e002000410064006f00620065002000520065006100640065007200200035002e0030002c0020006b0101002000610072012b00200074006f0020006a00610075006e0101006b0101006d002000760065007200730069006a0101006d002e> /NLD (Gebruik deze instellingen om Adobe PDF-documenten te maken die zijn geoptimaliseerd voor prepress-afdrukken van hoge kwaliteit. De gemaakte PDF-documenten kunnen worden geopend met Acrobat en Adobe Reader 5.0 en hoger.) /NOR <FEFF004200720075006b00200064006900730073006500200069006e006e007300740069006c006c0069006e00670065006e0065002000740069006c002000e50020006f0070007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740065007200200073006f006d00200065007200200062006500730074002000650067006e0065007400200066006f00720020006600f80072007400720079006b006b0073007500740073006b00720069006600740020006100760020006800f800790020006b00760061006c0069007400650074002e0020005000440046002d0064006f006b0075006d0065006e00740065006e00650020006b0061006e002000e50070006e00650073002000690020004100630072006f00620061007400200065006c006c00650072002000410064006f00620065002000520065006100640065007200200035002e003000200065006c006c00650072002000730065006e006500720065002e> /POL <FEFF0055007300740061007700690065006e0069006100200064006f002000740077006f0072007a0065006e0069006100200064006f006b0075006d0065006e007400f300770020005000440046002000700072007a0065007a006e00610063007a006f006e00790063006800200064006f002000770079006400720075006b00f30077002000770020007700790073006f006b00690065006a0020006a0061006b006f015b00630069002e002000200044006f006b0075006d0065006e0074007900200050004400460020006d006f017c006e00610020006f007400770069006500720061010700200077002000700072006f006700720061006d006900650020004100630072006f00620061007400200069002000410064006f00620065002000520065006100640065007200200035002e0030002000690020006e006f00770073007a0079006d002e> /PTB <FEFF005500740069006c0069007a006500200065007300730061007300200063006f006e00660069006700750072006100e700f50065007300200064006500200066006f0072006d00610020006100200063007200690061007200200064006f00630075006d0065006e0074006f0073002000410064006f0062006500200050004400460020006d00610069007300200061006400650071007500610064006f00730020007000610072006100200070007200e9002d0069006d0070007200650073007300f50065007300200064006500200061006c007400610020007100750061006c00690064006100640065002e0020004f007300200064006f00630075006d0065006e0074006f00730020005000440046002000630072006900610064006f007300200070006f00640065006d0020007300650072002000610062006500720074006f007300200063006f006d0020006f0020004100630072006f006200610074002000650020006f002000410064006f00620065002000520065006100640065007200200035002e0030002000650020007600650072007300f50065007300200070006f00730074006500720069006f007200650073002e> /RUM <FEFF005500740069006c0069007a00610163006900200061006300650073007400650020007300650074010300720069002000700065006e007400720075002000610020006300720065006100200064006f00630075006d0065006e00740065002000410064006f006200650020005000440046002000610064006500630076006100740065002000700065006e0074007200750020007400690070010300720069007200650061002000700072006500700072006500730073002000640065002000630061006c006900740061007400650020007300750070006500720069006f006100720103002e002000200044006f00630075006d0065006e00740065006c00650020005000440046002000630072006500610074006500200070006f00740020006600690020006400650073006300680069007300650020006300750020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e00300020015f00690020007600650072007300690075006e0069006c006500200075006c0074006500720069006f006100720065002e> /RUS <FEFF04180441043f043e043b044c04370443043904420435002004340430043d043d044b04350020043d0430044104420440043e0439043a043800200434043b044f00200441043e043704340430043d0438044f00200434043e043a0443043c0435043d0442043e0432002000410064006f006200650020005000440046002c0020043c0430043a04410438043c0430043b044c043d043e0020043f043e04340445043e0434044f04490438044500200434043b044f00200432044b0441043e043a043e043a0430044704350441044204320435043d043d043e0433043e00200434043e043f0435044704300442043d043e0433043e00200432044b0432043e04340430002e002000200421043e043704340430043d043d044b04350020005000440046002d0434043e043a0443043c0435043d0442044b0020043c043e0436043d043e0020043e0442043a0440044b043204300442044c002004410020043f043e043c043e0449044c044e0020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200431043e043b043504350020043f043e04370434043d043804450020043204350440044104380439002e> /SKY <FEFF0054006900650074006f0020006e006100730074006100760065006e0069006100200070006f0075017e0069007400650020006e00610020007600790074007600e100720061006e0069006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b0074006f007200e90020007300610020006e0061006a006c0065007001610069006500200068006f0064006900610020006e00610020006b00760061006c00690074006e00fa00200074006c0061010d00200061002000700072006500700072006500730073002e00200056007900740076006f00720065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f00740076006f00720069016500200076002000700072006f006700720061006d006f006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076016100ed00630068002e> /SLV <FEFF005400650020006e006100730074006100760069007400760065002000750070006f0072006100620069007400650020007a00610020007500730074007600610072006a0061006e006a006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b006900200073006f0020006e0061006a007000720069006d00650072006e0065006a016100690020007a00610020006b0061006b006f0076006f00730074006e006f0020007400690073006b0061006e006a00650020007300200070007200690070007200610076006f0020006e00610020007400690073006b002e00200020005500730074007600610072006a0065006e006500200064006f006b0075006d0065006e0074006500200050004400460020006a00650020006d006f0067006f010d00650020006f0064007000720065007400690020007a0020004100630072006f00620061007400200069006e002000410064006f00620065002000520065006100640065007200200035002e003000200069006e0020006e006f00760065006a01610069006d002e> /SUO <FEFF004b00e40079007400e40020006e00e40069007400e4002000610073006500740075006b007300690061002c0020006b0075006e0020006c0075006f00740020006c00e400680069006e006e00e4002000760061006100740069007600610061006e0020007000610069006e006100740075006b00730065006e002000760061006c006d0069007300740065006c00750074007900f6006800f6006e00200073006f00700069007600690061002000410064006f0062006500200050004400460020002d0064006f006b0075006d0065006e007400740065006a0061002e0020004c0075006f0064007500740020005000440046002d0064006f006b0075006d0065006e00740069007400200076006f0069006400610061006e0020006100760061007400610020004100630072006f0062006100740069006c006c00610020006a0061002000410064006f00620065002000520065006100640065007200200035002e0030003a006c006c00610020006a006100200075007500640065006d006d0069006c006c0061002e> /SVE <FEFF0041006e007600e4006e00640020006400650020006800e4007200200069006e0073007400e4006c006c006e0069006e006700610072006e00610020006f006d002000640075002000760069006c006c00200073006b006100700061002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400200073006f006d002000e400720020006c00e4006d0070006c0069006700610020006600f60072002000700072006500700072006500730073002d007500740073006b00720069006600740020006d006500640020006800f600670020006b00760061006c0069007400650074002e002000200053006b006100700061006400650020005000440046002d0064006f006b0075006d0065006e00740020006b0061006e002000f600700070006e00610073002000690020004100630072006f0062006100740020006f00630068002000410064006f00620065002000520065006100640065007200200035002e00300020006f00630068002000730065006e006100720065002e> /TUR <FEFF005900fc006b00730065006b0020006b0061006c006900740065006c0069002000f6006e002000790061007a006401310072006d00610020006200610073006b013100730131006e006100200065006e0020006900790069002000750079006100620069006c006500630065006b002000410064006f006200650020005000440046002000620065006c00670065006c0065007200690020006f006c0075015f007400750072006d0061006b0020006900e70069006e00200062007500200061007900610072006c0061007201310020006b0075006c006c0061006e0131006e002e00200020004f006c0075015f0074007500720075006c0061006e0020005000440046002000620065006c00670065006c0065007200690020004100630072006f006200610074002000760065002000410064006f00620065002000520065006100640065007200200035002e003000200076006500200073006f006e0072006100730131006e00640061006b00690020007300fc007200fc006d006c00650072006c00650020006100e70131006c006100620069006c00690072002e> /UKR <FEFF04120438043a043e0440043804410442043e043204430439044204350020044604560020043f043004400430043c043504420440043800200434043b044f0020044104420432043e04400435043d043d044f00200434043e043a0443043c0435043d044204560432002000410064006f006200650020005000440046002c0020044f043a04560020043d04300439043a04400430044904350020043f045604340445043e0434044f0442044c00200434043b044f0020043204380441043e043a043e044f043a04560441043d043e0433043e0020043f0435044004350434043404400443043a043e0432043e0433043e0020043404400443043a0443002e00200020042104420432043e04400435043d045600200434043e043a0443043c0435043d0442043800200050004400460020043c043e0436043d04300020043204560434043a0440043804420438002004430020004100630072006f006200610074002004420430002000410064006f00620065002000520065006100640065007200200035002e0030002004300431043e0020043f04560437043d04560448043e04570020043204350440044104560457002e> /ENU (Use these settings to create Adobe PDF documents best suited for high-quality prepress printing. Created PDF documents can be opened with Acrobat and Adobe Reader 5.0 and later.) >> /Namespace [ (Adobe) (Common) (1.0) ] /OtherNamespaces [ << /AsReaderSpreads false /CropImagesToFrames true /ErrorControl /WarnAndContinue /FlattenerIgnoreSpreadOverrides false /IncludeGuidesGrids false /IncludeNonPrinting false /IncludeSlug false /Namespace [ (Adobe) (InDesign) (4.0) ] /OmitPlacedBitmaps false /OmitPlacedEPS false /OmitPlacedPDF false /SimulateOverprint /Legacy >> << /AddBleedMarks false /AddColorBars false /AddCropMarks false /AddPageInfo false /AddRegMarks false /ConvertColors /ConvertToCMYK /DestinationProfileName () /DestinationProfileSelector /DocumentCMYK /Downsample16BitImages true /FlattenerPreset << /PresetSelector /MediumResolution >> /FormElements false /GenerateStructure false /IncludeBookmarks false /IncludeHyperlinks false /IncludeInteractive false /IncludeLayers false /IncludeProfiles false /MultimediaHandling /UseObjectSettings /Namespace [ (Adobe) (CreativeSuite) (2.0) ] /PDFXOutputIntentProfileSelector /DocumentCMYK /PreserveEditing true /UntaggedCMYKHandling /LeaveUntagged /UntaggedRGBHandling /UseDocumentProfile /UseDocumentBleed false >> ] >> setdistillerparams << /HWResolution [2400 2400] /PageSize [612.000 792.000] >> setpagedevice
id	nasplib_isofts_kiev_ua-123456789-82950
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn	0130-5395
language	Russian
last_indexed	2025-12-07T18:59:11Z
publishDate	2011
publisher	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
record_format	dspace
spelling	Анисимов, А.В. Джебелян, Т. Лялецкий, А.В. Попов, Н. 2015-06-12T09:13:14Z 2015-06-12T09:13:14Z 2011 Системы Theorema и автоматизация дедукции: сравнительный анализ / А.В. Анисимов, Т. Джебелян, А.В. Лялецкий. Н. Попов // Управляющие системы и машины. — 2011. — № 4. — С. 59-63, 77. — Бібліогр.: 20 назв. — рос. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/82950 004.8:510.62:63 Рассмотрены основные парадигмы обработки математических знаний и обозначено место среди них систем Theorema и автоматизация дедукции. Описаны сравнительный анализ систем, общие черты их построения и различие в методах обработки данных. Basic paradigms of the mathematical knowledge processing are considered and the place of the Theorema and SAD systems is outlined. A comparative analysis of the systems, common features of their construction and the distinction in data processing methods are described. Розглянуто основні парадигми обробки математичних знань та позначено місце серед них систем Theorema та автоматизація дедукції. Описано порівняльний аналіз систем, загальні риси їх побудови та різницю в методах обробки даних. ru Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Управляющие системы и машины Организационные и методические аспекты обеспечения непрерывного образования Системы Theorema и автоматизация дедукции: сравнительный анализ Theorema and SAD Systems: A Comparative Analysis Системи Theorema та автоматизація дедукції: порівняльний аналіз Article published earlier
spellingShingle	Системы Theorema и автоматизация дедукции: сравнительный анализ Анисимов, А.В. Джебелян, Т. Лялецкий, А.В. Попов, Н. Организационные и методические аспекты обеспечения непрерывного образования
title	Системы Theorema и автоматизация дедукции: сравнительный анализ
title_alt	Theorema and SAD Systems: A Comparative Analysis Системи Theorema та автоматизація дедукції: порівняльний аналіз
title_full	Системы Theorema и автоматизация дедукции: сравнительный анализ
title_fullStr	Системы Theorema и автоматизация дедукции: сравнительный анализ
title_full_unstemmed	Системы Theorema и автоматизация дедукции: сравнительный анализ
title_short	Системы Theorema и автоматизация дедукции: сравнительный анализ
title_sort	системы theorema и автоматизация дедукции: сравнительный анализ
topic	Организационные и методические аспекты обеспечения непрерывного образования
topic_facet	Организационные и методические аспекты обеспечения непрерывного образования
url	https://nasplib.isofts.kiev.ua/handle/123456789/82950
work_keys_str_mv	AT anisimovav sistemytheoremaiavtomatizaciâdedukciisravnitelʹnyianaliz AT džebelânt sistemytheoremaiavtomatizaciâdedukciisravnitelʹnyianaliz AT lâleckiiav sistemytheoremaiavtomatizaciâdedukciisravnitelʹnyianaliz AT popovn sistemytheoremaiavtomatizaciâdedukciisravnitelʹnyianaliz AT anisimovav theoremaandsadsystemsacomparativeanalysis AT džebelânt theoremaandsadsystemsacomparativeanalysis AT lâleckiiav theoremaandsadsystemsacomparativeanalysis AT popovn theoremaandsadsystemsacomparativeanalysis AT anisimovav sistemitheoremataavtomatizacíâdedukcííporívnâlʹniianalíz AT džebelânt sistemitheoremataavtomatizacíâdedukcííporívnâlʹniianalíz AT lâleckiiav sistemitheoremataavtomatizacíâdedukcííporívnâlʹniianalíz AT popovn sistemitheoremataavtomatizacíâdedukcííporívnâlʹniianalíz

Системы Theorema и автоматизация дедукции: сравнительный анализ

Institution

Similar Items