метод резолюций в исчислении высказываний

метод резолюций в исчислении высказываний Содержание. Введение………………………………….……………………………….3 1. Основные производители……………………………………………..5 2. История возникновения и развития языка ПРОЛОГ……….……….6 3. Исчисление высказываний…………………………………....………9  3.1. Исчисление предикатов…………………………………………….11  3.2. Программирование на ПРОЛОГЕ…………………………………14  3.3. Принцип резолюций……………………………………..…………16  3.4. Поиск доказательства в системе резолюций………………….…..18  Заключение……………………………………………………………….22 Список литературы………..…………………………………………..…24Введение. Программные   средства,   базирующиеся   на   технологии   и   методах искусственного интеллекта, получили значительное распространение в мире. Их важность, и, в первую очередь, экспертных систем и нейронных сетей, состоит   в   том,   что   данные   технологии   существенно   расширяют   круг практически значимых задач, которые можно решать на компьютерах, и их решение   приносит   значительный   экономический   эффект.   В   то   же   время, технология   экспертных   систем   является   важнейшим   средством   в   решении глобальных   проблем   традиционного   программирования:   длительность   и, следовательно,   высокая   стоимость   разработки   приложений;   высокая стоимость   сопровождения   сложных   систем;   повторная   используемость программ и т.п. Кроме того, объединение технологий экспертных систем и нейронных сетей с технологией традиционного программирования добавляет новые качества к коммерческим продуктам за счет обеспечения динамической модификации   приложений   пользователем,   а   не   программистом,   большей "прозрачности"   приложения   (например,   знания   хранятся   на   ограниченном естественном языке, что не требует комментариев к ним, упрощает обучение и   сопровождение),   лучших   графических   средств,   пользовательского интерфейса и взаимодействия. По мнению специалистов, в недалекой перспективе экспертные системы будут   играть   ведущую   роль   во   всех   фазах   проектирования,   разработки, производства,   распределения,   продажи,   поддержки   и   оказания   услуг.   Их технология,   обеспечит революционный   прорыв   в   интеграции   приложений   из   готовых   получив   коммерческое   распространение, интеллектуально­взаимодействующих модулей. 3Среди   специализированных   систем,  основанных   на   знаниях,  наиболее значимы   экспертные   системы   реального   времени,   или   динамические экспертные системы. На их долю приходится 70 процентов этого рынка. Значимость инструментальных средств реального времени определяется не   столько   их   бурным   коммерческим   успехом   (хотя   и   это   достойно тщательного   анализа),   но,   в   первую   очередь,   тем,   что   только   с   помощью подобных   средств   создаются   стратегически   значимые   приложения   в   таких областях,  как   управление   непрерывными   производственными   процессами   в химии,   фармакологии,   производстве   цемента,   продуктов   питания   и   т.п., аэрокосмические исследования, транспортировка и переработка нефти и газа, управление атомными и тепловыми электростанциями, финансовые операции, связь и многие другие. Классы   задач,  решаемых   экспертными   системами   реального  времени, таковы:   мониторинг   в   реальном   масштабе   времени,   системы   управления верхнего   уровня,   системы   обнаружения   неисправностей,   диагностика, составление   расписаний,   планирование,   оптимизация,   системы­советчики оператора, системы проектирования. Коммерческие   успехи   к   экспертным   системам   и   нейронным   сетям пришли не сразу. На протяжении ряда лет (с 1960­х годов) успехи касались в основном   исследовательских   разработок,   демонстрировавших   пригодность систем   искусственного   интеллекта   для   практического   использования. Начиная примерно с 1985 (а в массовом  масштабе, вероятно, с 1988­1990 годов),   в   первую   очередь,   экспертные   системы,   а   в   последние   два   года   и нейронные сети стали активно использоваться в реальных приложениях. 41. Основные производители. Инструментарий   для  создания   экспертных   систем   реального  времени впервые   выпустила   фирма   Lisp   Machine   Inc   в   1985   году.   Этот   продукт предназначался для символьных ЭВМ Symbolics и носил название Picon. Его успех   привел   к   тому,   что   группа   ведущих   его   разработчиков   образовала фирму   Gensym,   которая,   значительно   развив   идеи,   заложенные   в   Picon, выпустила   в   1988   году   инструментальное   средство   под   названием   G2.   В настоящий момент работает его третья версия и подготовлена четвертая. Еще в конце 1970­х годов стала отчетливо просматриваться тенденция к использованию   в   исследованиях   в   области   искусственного   интеллекта "формальных" методов, т.е. основанных на аппарате математической логики. Эти   методы   противопоставлялись   более   интуитивным   и   менее формализованным   эвристическим   методам,   скажем,   таким,   которые   были использованы   в  системе  MYCIN.  Для   того   чтобы   стало   ясно,  что   все   это значит, нужно познакомить вас с логическими языками, а затем показать, как соотносятся   их   свойства   с   теми   методами   рассуждений,   которые   должны поддерживать типовые экспертные системы. Математическая логика является формальным языком в том смысле, что в отношении любой последовательности символов она позволяет сказать, удовлетворяет   ли   эта   последовательность   правилам   конструирования выражений   в   этом   языке   (формулам).   Обычно   формальным   языкам противопоставляются естественные, такие как французский и английский, в которых грамматические правила не являются жесткими. Утверждение, что логика является исчислением с определенными синтаксическими правилами логического вывода, означает, что влияние одних членов выражения на другие зависит только от формы выражения в данном языке и ни коим образом не зависит от каких­либо посторонних идей или интуитивных предположений. 5Под автоматическим формированием суждений понимается поведение некоторой компьютерной программы, которая строит логический вывод на основании   определенных   законов.   Так,   нельзя   отнести   к   классу   программ автоматического   формирования   суждений   программу,   которая   моделирует подбрасывание   монетки,   чтобы   определить,   следует   ли   одна   формула   из набора   других.   (В   литературе   также   часто   встречается   термин автоматическая дедукция, равнозначный по смыслу термину автоматическое формирование суждений.) При реализации автоматического формирования суждений, как правило, стремятся   к   максимально   возможному   единообразию   и   стандартизации   в представлении   формул,   но   в   то   же   время   в   литературе   часто   приходится сталкиваться с самыми разнообразными системами обозначений, относящихся к   логике.   Основными   синтаксическими   схемами   представления   выражений являются конъюнктивная нормальная форма (conjunctive normal form— CNF), полная   фразовая   форма   (full   clausal   form)   и   фраза   Хорна   (Horn   clause), последняя является подмножеством полной фразовой формы.  62. История возникновения и развития языка ПРОЛОГ.   На   протяжении   многих   тысячелетий   человечество   занимается накоплением,  обработкой  и   передачей  знаний.  Для   этих   целей   непрерывно изобретаются   новые   средства   и   совершенствуются   старые:   речь, письменность, почта, телеграф, телефон и т. д. Большую роль в технологии обработки знаний сыграло появление компьютеров. В октябре 1981 года Японское министерство международной торговли и промышленности объявило о создании исследовательской организации — Института по разработке методов создания компьютеров нового поколения (Institute for New Generation Computer Technology Research Center).  Целью данного проекта было создание систем обработки информации, базирующихся на знаниях. Предполагалось, что эти системы будут обеспечивать простоту управления   за   счет   возможности   общения   с   пользователями   при   помощи естественного языка. Эти системы должны были самообучаться, использовать накапливаемые   в   памяти   знания   для   решения   различного   рода   задач, предоставлять   пользователям   экспертные   консультации,   причем   от пользователя   не   требовалось   быть   специалистом   в   информатике. Предполагалось, что  человек  сможет  использовать  ЭВМ  пятого поколения так   же   легко,   как   любые   бытовые   электроприборы   типа   телевизора, магнитофона и пылесоса. Вскоре вслед за японским стартовали американский и европейский проекты. Появление   таких   систем   могло   бы   изменить   технологии   за   счет использования баз знаний и экспертных систем. Основная суть качественного перехода к пятому поколению ЭВМ заключалась в переходе от обработки данных   к   обработке   знаний.   Японцы   надеялись,   что   им   удастся   не подстраивать   мышление   человека   под   принципы   функционирования компьютеров, а приблизить работу компьютера к тому, как мыслит человек, 7отойдя при  этом от фон  неймановской архитектуры  компьютеров.  В 1991 году   предполагалось   создать   первый   прототип   компьютеров   пятого поколения. Теперь уже понятно, что поставленные цели в полной мере так и не были достигнуты, однако этот проект послужил импульсом к развитию нового витка   исследований   в   области   искусственного   интеллекта   и   вызвал   взрыв интереса   к   логическому   программированию.   Так   как   для   эффективной реализации традиционная фон неймановская архитектура не подходила, были созданы специализированные компьютеры логического программирования PSI и PIM. В качестве основной методологии разработки программных средств для проекта ЭВМ пятого поколения было избрано логическое программирование, ярким представителем  которого является язык Пролог. Думается, что и в настоящее   время   Пролог   остается   наиболее   популярным   языком искусственного интеллекта в Японии и Европе (в США, традиционно, более распространен   другой   язык   искусственного   интеллекта   ­   язык функционального программирования Лисп). Название   языка   "Пролог"   происходит   от   слов   ЛОГическое ПРОграммирование (PROgrammation en LOGique во французском варианте и PROgramming in LOGic — в английском). Пролог   основывается   на   таком   разделе   математической   логики,   как   его   базис   составляет   процедура исчисление   предикатов.   Точнее, доказательства теорем методом резолюции для хорновских дизъюнктов.  В   истории   возникновения   и   развития   языка   Пролог   можно   выделить следующие этапы. В 1965 году в работе "A machine oriented logic based on the resolution principle", опубликованной в 12 номере журнала "Journal of the ACM", Дж Робинсон представил метод автоматического поиска доказательства теорем в исчислении   предикатов   первого   порядка,   получивший   название   "принцип 8резолюции". На самом деле, идея данного метода была предложена Эрбраном в 1931 году, когда еще не было компьютеров. Робинсон модифицировал этот метод   так,   что   он   стал   пригоден   для   автоматического,   компьютерного использования,   и,   кроме   того,   разработал   эффективный   алгоритм унификации, составляющий базис его метода. В 1973  году "группа  искусственного  интеллекта" во  главе  с  Аланом Колмероэ создала в Марсельском университете программу, предназначенную для доказательства теорем. Эта программа использовалась при построении систем обработки текстов на естественном языке. Программа доказательства теорем   получила   название   Prolog   (от   Programmation   en   Logique).   Она   и послужила прообразом Пролога. Ходят легенды, что автором этого названия была   жена   Алана   Колмероэ.   Программа   была   написана   на   Фортране   и работала довольно медленно. Большое значение для развития логического программирования имела работа   Роберта   Ковальского   "Логика   предикатов   как   язык программирования" (Kowalski R. Predicate Logic as Programming Language. IFIP Congress, 1974),  в  которой   он   показал,  что   для  того  чтобы   добиться эффективности, нужно ограничиться использованием множества хорновских дизъюнктов. Кстати, известно, что Ковальский и Колмероэ работали вместе в течение одного лета. В 1976 г. Ковальский вместе с его коллегой Маартеном ван Эмденом предложил   два   подхода   к   прочтению   текстов   логических   программ: процедурный   и   декларативный.   Об   этих   подходах   речь   пойдет   в   третьей лекции. В 1977 году в Эдинбурге Уоррен и Перейра создали очень эффективный компилятор языка Пролог для ЭВМ DEC–10, который послужил прототипом для многих последующих реализаций Пролога. Что интересно, компилятор был   написан   на   самом   Прологе.   Эта   реализация   Пролога,   известная   как "эдинбургская версия", фактически стала первым и единственным стандартом 9языка. Алгоритм, использованный при его реализации, послужил прототипом для многих последующих реализаций языка. Как правило, если современная Пролог­система   и   не   поддерживает   эдинбургский   Пролог,   то   в   ее   состав входит подсистема, переводящая прологовскую программу в "эдинбургский" вид. Имеется, конечно, стандарт ISO/IEC 13211– 1:1995, но его поддерживают далеко не все Прологсистемы. В 1980 году Кларк и Маккейб в Великобритании разработали версию Пролога для персональных ЭВМ. В   1981   году   стартовал   вышеупомянутый   проект   Института   по разработке методов создания компьютеров нового поколения. На сегодня существует довольно много реализаций Пролога. Наиболее известные из них следующие: BinProlog, AMZI­Prolog, Arity Prolog, CProlog, Micro   Prolog,   МПролог,   Prolog­2,   Quintus   Prolog,   SICTUS   Prolog,   Silogic Knowledge Workbench, Strawberry Prolog, SWI Prolog, UNSW Prolog и т. д. В нашей стране были разработаны такие версии Пролога как Пролог­Д (Сергей Григорьев), Акторный Пролог (Алексей Морозов), а также Флэнг (А. Манцивода, Вячеслав Петухин). Стерлинг и Шапиро в книге "Искусство программирования на языке Пролог"   пишут:   "Зрелость   языка   означает,   что   он   больше   не   является доопределяемой и уточняемой научной концепцией, а становится реальным объектом   со   всеми   присущими   ему   пороками   и   добродетелями.   Настало время   признать,   что   хотя   Пролог   и   не   достиг   высоких   целей   логического программирования,   но,   тем   не   менее,   является   мощным,   продуктивным   и практически пригодным формализмом программирования". 103. Исчисление высказываний. Исчисление высказываний представляет собой логику неанализируемых предположений,   в   которой   пропозициональные   константы   могут рассматриваться   как   представляющие   определенные   простые   выражения вроде "Сократ — мужчина" и "Сократ смертен". Строчные литеры р, q, r, ... в дальнейшем   будут   использоваться   для   обозначения   пропозициональных констант, которые иногда называют атомарными формулами, или атомами. Ниже   приведены   все   синтаксические   правила,   которые   используются для конструирования правильно построенных формул (ППФ) в исчислении высказываний. (S. U) ЕслиU является атомом, то у является ППФ. (S¬) Если U является ППФ, то —U также является ППФ. (S. v) Если U и ф являются ППФ, то (U u ф) также является ППФ. В этих правилах строчные буквы греческого алфавита (например, U и ф) представляют пропозициональные переменные, т.е. не атомарные формулы, а любое простое или составное высказывание. Пропозициональные константы являются частью языка высказываний, который используется для приложения исчисления пропозициональных переменных к конкретной проблеме. Выражение ­U читается как "не U", а (U v ф) читается как дизъюнкция "U   или   ф   (или   оба)".   Можно   ввести   другие   логические   константы   —   "л" (конъюнкция), "D" (импликация, или обусловленность), "=" (эквивалентность, или   равнозначность),   которые,   по   существу,   являются   сокращениями комбинации трех приведенных выше констант. . (U ^ ф) Эквивалентно¬(¬U v ф). Читается "U и ф". (U  ф) Эквивалентно (¬U v ф). Читается "U имплицирует ф". (U==ф) Эквивалентно (U ф)^(ф U). Читается "U эквивалентно ф". 11В   конъюнктивной   нормальной   форме   исчисления   высказываний константы   "импликация"   и   "эквивалентность"   заменяются   константами "отрицание"   и   "дизъюнкция",   а   затем   отрицание   сложного   выражения раскрывается с помощью формул Де Моргана: ¬(U^ф) преобразуется в (¬Uv¬ф), ¬(U v ф) преобразуется в (­U^ф) , ¬¬U преобразуется в U . Последний этап преобразований — внесение дизъюнкций внутрь скобок: (£ v (U ^ф))) заменяется ((£vU\(U)^(£vф)). Принято   сокращать   вложенность   скобочных   форм,   отбрасывая   в нормальной конъюнктивной форме знаки операций v и л. Ниже представлен пример   преобразования   выражения,   содержащего   импликацию   двух скобочных форм, в нормальную конъюнктивную форму. ¬(pvq) (­p^A­q) Исходное выражение. ¬¬(pvg)v(­p^­ q) Исключение~. (pvq)v(­p^­ q) Ввод ­ внутрь скобок. (¬pv(pvq))v(¬pv(pvq)) Занесение v внутрь скобок. {{­p,   р,   q},   {¬q,   р,   q}   }   Отбрасывание   А   и   v   в   конъюнктивной нормальной форме. Выражения во внутренних скобках — это либо атомарные формулы, либо   негативные   атомарные   формулы.  Выражения   такого   типа   называются литералами, причем с точки зрения формальной логики порядок литералов не имеет значения. Следовательно, для представления множества литералов — фразы   —   можно   позаимствовать   из   теории   множеств   фигурные   скобки. Литералы   в   одной   и   той   же   фразе   неявно   объединяются   дизъюнкцией,   а фразы, заключенные в фигурные скобки, неявно объединяются конъюнкцией. Фразовая форма очень похожа на конъюнктивную нормальную форму, за   исключением   того,   что   позитивные   и   негативные   литералы   в   каждой дизъюнкции группируются вместе по разные стороны от символа стрелки, а 12затем   символ   отрицания   отбрасывается.   Например,   приведенное   выше выражение преобразуется в две фразы: p,q<¬q. в которых позитивные литералы сгруппированы слева от знака стрелки, а негативные справа. Более строго, фраза представляет собой выражение вида в котором p1..., рт q1,..., qn являются атомарными формулами, причем т=>0   и   п=>0.   Атомы   в   множестве   р1,...,   рт   представляют   заключения, объединенные операторами дизъюнкции, а атомы в множестве q1 ..., qn — условия, объединенные операторами конъюнкции. 3.1 Исчисление предикатов Исчисление   высказываний   имеет   определенные   ограничения.   Оно   не позволяет   оперировать   с   обобщенными   утверждениями   вроде   "Все   люди смертны".   Конечно,   можно   обозначить   такое   утверждение   некоторой пропозициональной   константой   р,   а   другой   константой   q   обозначить утверждение "Сократ — человек". Но из (р л q) нельзя вывести утверждение "Сократ смертен". Для этого нужно анализировать пропозициональные символы в форме предикатов   и   аргументов,   кванторов   и   квантифщированных   переменных. Логика   предикатов   предоставляет   нам   набор   синтаксических   правил, позволяющих   выполнить   такой   анализ,   набор   семантических   правил,   с помощью которых интерпретируются эти выражения, и теорию доказательств, которая позволяет вывести правильные формулы, используя синтаксические правила   дедукции.   Предикатами   обозначаются   свойства,   такие   как   "быть человеком", и отношения, такие как быть "выше, чем". 13Аргументы   могут   быть   отдельными   константами,   или   составным выражением "функция­аргумент", которое обозначает сущности некоторого мира   интересующих   нас   объектов,   или   отдельными   квантифицируемыми переменными,   которые   определены   в   этом   пространстве   объектов. Специальные   операторы   —   кванторы   —   используются   для   связывания переменных   и   ограничения   области   их   интерпретации.   Стандартными являются   кванторы   общности   (V)   и   существования   (3).   Первый интерпретируется как "все", а второй — "кое­кто" (или "кое­что"). Ниже   приведены   синтаксические   правила   исчисления   предикатов первого порядка. Любой символ (константа или переменная) является термом. Если rk является символом k­местной функции и а1 ...,