WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |   ...   | 22 |

Здесь в первую очередьследует отметить хорошо известный методрезолюции [15], а также вышеупомянутыепруверы, используемые в системе САД.Попытки воспользоваться подходомрезолюционного типа для построения другихметодов автоматизации поиска логическоговывода в последующем привели к появлениюцелого ряда разнообразной техники поискалогического вывода, например, методаэлиминации моделей, метода графа связей,табличных методов и т.п. Мы отсылаем кисчерпывающему справочнику [16], вкотором заинтересованный читатель можетнайти почти все последние достижения поэффективным методам автоматизациирассуждений для классической логикипервого порядка, но все-таки требующимпроведения предварительной сколемизации.Несмотря на высокую эффективностьпроцесса установления выводимости, ихотрицательным качеством является то, чтовсе они все же не дают возможностиосуществлять процесс машинногодоказательства в соответствии стребованиями к дедукции, перечисленнымвыше.

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

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

В случае историческисложившегося, классического подхода можновыделить два типа допустимостиподстановок для секвенциальныхисчислений: генценовское [9] и кангеровское[10] понятия, которые являютсянеудовлетворительными с точки зрения ихиспользования в машинно-ориентированныхсеквенциальных исчислениях. Поэтому былапредпринята попытка [17] изменить понятиедопустимой подстановки так, чтобы добитьсяопределенной оптимизацию кванторныхприменений, ведущей к существенномуповышению эффективности поискалогического вывода в секвенциальныхисчислениях. В дальнейшем, это новоепонятие было инкорпорировано в рядсеквенциальных исчислений, специальнопостроенных для эффективизации процессадедукции в случае отказа от сколемизации(см., например, [18,19]). И именно этотподход2 был использован при реализациилогического аппарата системы САД, чтосущественно отличает ее от других систем,базирующихся на секвенциальном илитабличном формализмах.

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

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

Заключение. Система САДможет служить основой для построениясистем поддержки рассуждений вформализованных теориях; она может бытьнастроена на поиск решений различныхприкладных задач, допускающих ихформализацию в логике первого порядка. Вчастности, можно указать следующие областиее применения:

  • компьютерная помощь в обученииматематике и логике;
  • удаленное (дистанционное) обучениематематическим дисциплинам;
  • доказательство теорем и верификацияформализованных (математических)текстов;
  • извлечение знаний из математическихпубликаций;
  • построение баз знаний дляформализованных теорий.

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

Литература

  1. Глушков В.М. Некоторые проблемытеории автоматов и искус-ственногоинтеллекта. // Кибернетика. - 1970. - № 2. - C.3-13.
  2. Verchinine, K., Lyaletski, A., and Paskevich, A. System forAutomated Deduction (SAD): a tool for proof verification. In AutomatedDeduction // Lecture Notes in Computer Science, Springer. V. 4603. 2007. P. 398-403.
  3. Anisimov A. and Lyaletski A. The SAD system in three dimensions //Proceedings of the SYNASC'06. Timisoara, Romania. 2006. P.85-88.
  4. Vershinin K., Paskevich A. ForTheL the language of formal theories //International Journal of Information Theories and Applications 2000. 7, № 3. P. 120-126.
  5. Анисимов А.В., Бычков А.С., КлименкоВ.П.

    и Лялецкий А.В. О типахинтеллектуального тестирования знаний впроцессе электронного обучения // Збірникпраць Другої Міжнародної конференції "Новіінформаційні технології в освіті для всіх:стан та перспективи розвитку". Київ. 21-23 листопада 2007. С. 366-373.

  6. The SPASS Prover. http://spass.mpi-sb.mpg.de/
  7. The Vampire prover. http://www.cs.man.ac.uk/~riazanoa/Vampire/
  8. The Otter prover. http://www.mcs.anl.gov/ AR/otter/
  9. Gentsen G. Untersuchungen uber das logische Schlieben //Mathematische Zeitschruft. v. 39 (I, II). 1934-1935. P. 176-210, 405-443.
  10. Kanger S. Simplified Proof Method for Elementary Logic // ComputerProgramming and Formal Systems: Studies in Logic. Amsterdam: North-Holland Publ. Co. 1963. P. 87-93.
  11. Ануфриев Ф.В. Алгоритм поискадоказательств теорем в логическихисчислениях // Теория автоматов. Киев: Изд-во ИК АНУССР. Вып. 5, №1. 1969. P. 3-26.
  12. АнуфриевФ.В., Федюрко В.В.,Летичевский А.А., Асельдеров З.М., Дидух И.И.Об одном алгоритме поиска доказательствтеорем в теории групп // Кибернетика. -- 1966. № 1. С. 23-29.
  13. Skolem T. Logisch-kombinatorische Untersuchungen uberErfullbarkeit oder Beweisbarkeit mathematischer Stze nebst einem Theorem uber dichteMengen. // Skrifter utgit av Videnskapsselskape inKristiania. I. Mat.-Nat. Kl № 4. 1919. P.1-36.
  14. Herbrand J. Recherches sur la Theorie de la Demonstration //Travaux de la Societe des Sciences et des Lettres de Varsovie. >
  15. Robinson A. J. A Machine-Oriented Logic Based on ResolutionPrinciple // Journal of the ACM. V.12, № 1. 1965. P.23-41.
  16. Handbook of Automated reasoning / Eds.: Robinson A. and Voronkov A. Elsevier SciencePublishers B.V. V.1-2. 2001. 2184 pp.
  17. Lyaletski A. V. Gentzen calculi and admissible substitutions //Actes Preliminaieres du Symposium Franco-Sovietique "Informatika-91". Grenoble, France. 1991. P. 99-111.
  18. Degtyarev A., Lyaletski A., and Morokhovets M. Evidence Algorithmand Sequent Logical Inference Search // Lecture Notes in ArtificialIntelligence. 1705. 1999. P. 44-61.
  19. Лялецкий А.В. Эвиденциальнаяпарадигма: логический аспект // Кибернетикаи системный анализ. 2003. №5. С.37-47.
  20. Konev B. and Lyaletski A. Tableau Method with Free Variables forIntuitionistic Logic // Proceedings of the International IIS: IIPWM'06Conference. Advances in Soft Computing. V. 35. 2006. P. 153-162.
  21. Lyaletski A. On some problems of efficient inference searchin first-order cut-free modal sequent calculi. // Proceedings of the 10thInternational SYNASC 2008 Symposium. Timisoara, Romania. IEEE Inc. 2008. P.39-46.

LERNER MODEL AS AN OBJECT OF THE AUTOMATIZEDCONTROL

Mazurok Tatyana

Odessa National Polytechnic University,Ukraine

A lerner model is offered, which synergeticapproach of teaching management is realized. Neuron network realization of thismodel is resulted. It is supported by teaching multi-layered neuron network.

МОДЕЛЬ ОБУЧАЕМОГО, КАКОБЪЕКТА АВТОМАТИЗИРОВАННОГОУПРАВЛЕНИЯ

Мазурок Татьяна

Одесский национальныйполитехнический университет,Украина

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

Актуальность ипостановка задачи

Одной из характеристиксовременного образования являетсяиндивидуальная траектория обучения.Необратимой тенденцией образования винформационном обществе становится отходот детерминированных траекторий обученияв сторону их полной индивидуализации наоснове учёта всего спектра индивидуальныхособенностей, генетических способностей,целей обучения, располагаемых ресурсов ипр. Реформирование системы высшегообразования на основе“студенто-ориентированного” подходапутём внедрения индивидуальных траекторийстудентов [1] на Украине согласуется как стеоретическим обоснованием дидактическойцелесообразностииндивидуализированного обучения [2], так и сосновными целями международныхобразовательных проектов –Межправительственной программы ЮНЕСКО«Образование для всех» [3], Болонскойдекларации [4].

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

Преодоление данногопротиворечия, с нашей точки зрения,возможно на основе разработки моделейавтоматизированного управления процессомобучения, что требует адаптациисовременной теории управления кпотребностям образования.

Разработка моделей иметодов для разработки системавтоматизированного управленияиндивидуализированным обучениемпредставляет собой нерешённую проблему иопределяет актуальность данногоисследования.

Синергетический подходк управлению обучением

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

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

Такимобразом, учёт в процессе анализа«синергетических» свойств и особенностей,характерных для обучения, даёт возможностьопределить параметры процесса управленияобучением, адаптированного дляконкретного обучаемого.

Двухклассовая модельуправления обучением

Математические моделиуправления обучением [6], [7] могут получитьдальнейшее развитие в рамкахсинергетического подхода [5], еслиобъединить их понятийно-терминологическийаппарат. Такое объединение можно сделатьпри допущении об эквивалентностикоэффициентов забывания и умозаключения [6]соответствующим коэффициентаминдивидуальных особенностей [7], а такженайти связь между двумя параметрамиуправления: количеством информации S [6]и долей времени, отведённой накоплениюзнаний U [7].

Следуя терминологии [7],запишем

(1)

где a – объём накопленныхзнаний,

A – полный объём знаний,

b – объём накопленных умений,

B – полный объём умений,

x, y – нормированныеобъёмы знаний и уменийсоответственно.

Нормируя количествоинформации и разделяя её на два класса(знания и умения), получим:

или с учётом (6)

что равносильно

(2)

Согласно принятымобозначениям и определению U получим

откуда из (2)находим

Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |   ...   | 22 |






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»