Intel_Nils, страница 50

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

Стратегии, использующие семантику, можно построить различными способами, однако пока в этом направлении было предпринято не слишком много попыток, Возникает вопрос: нельзя ли воспользоваться оценочной функцией, заданной на парах предложений, являющихся кандидатами на разрешение? Возможно, она могла бы учитывать и 250 Гл. д. Метода ноиска доказатвльства в исчислении аредикатов имеющуюся семантическую информацию, и форму предложений- кандидатов. Некоторые теоретические результаты о свойствах стратегий с оценочными функциями содержатся в статье Ковальского (1970а).

Его результаты о поиске на структурах «графов вывода» аналогичны результатам Харта и др. (!968) для структур графов в пространстве состояний. Примеры реализации Уже написано несколько программ для автоматического до- казательства теорем. Например, программы Робинсона и Воса (1969), Аллена и Лакхэма (1970), Гарда и др. (1969), а также система Грина — Рафаэля — Р(ейтса, модифицированная Гар- веем и Клингом (1969). Задачи 8Л. Укажите, для каких из следующих предложений предложение Р(1(х),у) является подслучаем; а) Р (1 (а), 1 (х)) Ч Р (г, 1(у)), Ь) Р (г, а) Ч ' Р (а, г), с) Р () (Е (х)), г), д) Р ()(г), г) Ч 0 (к), е) Р (а, а) Ч Р (1 (к), у).

%2. Найдите опровержение в виде лозы для следующего невыполнимого множества предложений: а) РЧ-ЯЧВ, Ь) ЯЧТ, с) ТЧР, д) Я, е) Я, () ЗЧьГ, 8) (тЧФ ' Можете лн вы найти другие опровержения (не обязательно в виде йозы), имеющие меньшую глубину? 8.3. Найдите опровержение в АР-форме для следующего невыполнимого множества предложений: а) А(к) Ч Р(х) Ч 0()(х)), Ь) Р (х) Ч В (х), с) Р (х) Ч С (х), д) - а (х) Ч В (х), е) О (х) Ч В (х), )) А (у (х)) Ч Р (й (х)), к) В (х) Ч С (х), Ь) В (к) Ч В (х).

Сравните с ненмеющвм такую форму опровержением, приведенным не рис. 7.5, Задами 8А. Найдите коитрпример к утверждению: «Стратегия предпочтения одно- членам всегда позволяет найти опровержение минимальной глубины». 8.8. Рассмотрите задачу поиска опровержш>ия с' отфильтрованными предшествующими вершинами для невыполнимого множества 5 предложений как задачу перебора в пространстве состонний. Пусть описание состояния содержит дерево доказательства в АГ-форме и множество 5. а) Что служит начальной вершиной? б) Что представляет собой оператор построения дочерних вершин? в) Каков критерий достижения цели? г) Предложите оценочную функцию г, учитывающую уровень АГ-дерева, «общность» содержащихся в нем предложений, глубину размещения функций в его предложениях и другие фаиторы, которые вы считаете важными, 88.

Рассмотрите утверждение; «В замкнутой ассоциативной системе с левымн и правыми решениями уравнений существует единичный элемент». Условия можно выразить следующим образом: ЫхЫуВг Р (г, х, у) — для всех х и у в этой системе найдется такой элемент г нз этой системы, что г х = у; ыхыузг Р (х, г, в) — для всех х и р в втой системе найдется такой элемент г из этой системы, что х г = р; ЫхЫуВг Р (х, р.

г) — для всех х и у в этой системе найдется такой элемент г из этой системы, что хну г (замыкание); Ыиошхуг([Р (и, и, ш) Л Р (о, х, у)) =3> [Р (и, у, г) ~ Р (и, х, г))) (ассоциативность). (Замечание: А н«В — сокращенная запись для [(А =)ь В) Л (В р А)).) Заключение можно записать в виде ЭуЫх Р(х, у, г) — существует правый единичный элемент. Для этой теоремы сделайте следующее: а) Преобразуйте условия н отрицание заключения в форму предложений. б) С помощью этих предложений получите Р,-опровержение. в) Из этого опровержения извлеките ответное утверждение (т. е. получите выражение для правого единичного элемента). СПИСОК ЛИТЕРАТУРЫ АЛЛЕН, ЛАКХЭМ (АЬЬЕМ 3., Ы)СКНАМ О.) 1970,Ап 1п1егас1гче ТЬеогегп-РгоЫпй Рго8гаш, !и В.

Мейвег апй О. М1- сЫе (ейв.), кМасЬ!пе !п1е!ПБепсе 5», 321 — 336, Ашег!сап ЕЫеч!ег РиЫ!»Ып8 Сатрапу, Матч УогК. АМАРЕЛЬ (АМАКЕЬ Б.) 1965 РгоЫеш Бо!чгпд Ргоседигез 1ог ЕИс!еп! Буп1ас11с Апа!ув!в, АСМ 20ЬЬ Ма1!. Соп1. [см. такие Бс!. Кер1. Мо. 1, АГОБК Соп1г. Мо. АГ49(638) ° 1184, !968). 1966 Маге оп йергезеп1аПопз о1 Ьйе Мопйеу РгоЫеш, Сагпей!е !пз1Пи1е о1 Тесйпо!ойу Ьес1иге Ма1ез, Магсй 1, !967 Ап Арргоасй 1о НеигЫПс РгоЫеш-Бо!ч!пй апй ТЬеогеш Ргоч!пй )п Ьйе РгороЫПопа! Са!си!из, !п Л Наг1 апй Б.

Тайави (ейз,), «Буйегпв апб Сошри1ег Бс!епсе», ~Зп!четв!(у о( Тогой1о Ргезв, Тогоп1о. !968 Оп йергевеп1а1!опз о( РгоЫегпз о! Кеазоп!пд АЬои1 Ас11опв, 1п О. МгсЬге (ед.), «МасЬгпе !п(е!Пйепсе 3», !31 — !71, Агпепсап Е!веч!ег РиЫЫЬ. !пй Сошрапу, 1йс., Мети Уогй !969 Оп 1Ье йергезеп1а1!оп о1 РгоЫешз апд боа! Ойес!ей Ргосейигев (ог Сошри1егз, Саттип. Ат. Бос.

Суйегпез!сз, 1, Ма. 2. АНДЕРСОН, БЛЕДСОУ (АМОЕКБОМ й., ВЬЕОБОЕ Уч'.) !970 А ййпеаг Гогша1 1ог йезо!иПап кч!1Ь Мегй!пи апй а Мети ТесЬпЬ йие 1ог ЕЫаЫЫЬ!пй Сошр!е(епезв, А АСМ, 17, Мо. 3. БАР ХИЛЛЕЛ (ВАК Н1ЬЬЕЬ Х.) 1969 ЬГп!четка! БешапПсв апд РЫ1оворйу О1 Ьапииайе: Оиапйаг!ез апй Ргозрес1в, !п сввп Рийче! (ей,), «БиЬз1апсе апй 51гис(иге о1 Ьапйиаие», 1)п1- чегзПу о1 Сай(огп!а Ргезз, Вегйе!еу. БЕЛЛМАН, ДРЕИФУС (ВЕЬЬМАМ К., ОКЕУГЬгБ Б,) !962 АррйеП Оупаш!с Ргойгашш)п8, Рг!псе1оп 1)п!четв!(у Ргевв, Рпп- се(оп, М. Л [Русский перевод: Прикладные задачи динамического программи.

раввина, «Наука», М., 1965) БЕЛЛМОР, НЕМХОЗЕР (ВЕЬЬМОКЕ М., МЕМНАЫБЕК О.) 1968 ТЬе Тгачейп8 Ба!езшап РгоЫеш: А Бигчеу, Орегойопз йез., 16, Мо. 3, 538 — 558. БЕНЕРДЖИ (ВАМЕКЛ К,) 1969 ТЬеогу о1 РгоЫеш Бо!ч!пйи Ап Арргоасй 1о Аг1П!с!а! 1п1еП!иепсе, Ашепсап ЕВеч!ег РиЬПвЫпй Сатрапу, !пс., Метч Уогй [Русский перевод. Теория решения задач. Подход к созданиго искусственного интеллекта, «Мнр», М., 1972.) БЕР7К (ВЕКОЕ С.) !958 ТЬе ТЬеогу о1 Огарйв апд 'Пв Аррйса!!опв, Оппеле, РагЫ (на франц. яз.). [Русский перевод: Теория графов и ее применения, ИЛ, М., 1962.) Список литературы БЕРНШТЕЙН н др, (ВЕКХБТЕ!Х А.

е1 аЦ 1958 А СЬевв-Р1ау1пд Ргодгага (ог йе.!ВМ 704 Согпри1ег, Ргос. 1уев(. уогп! Согари1ег Соп1., рр. !57 — 159. БЛЭК (ВЬАСК Р.) 1964 А РедисБче ОиевБап-Апвмег!пд БуЫею, Рос!ага! Р!вьет!а(1оп, Нагчагд. См. также М. М!пану (ей.), «БегаапБс 1п(оппаБоп Ргасевв!п6», 354 — 402, ТЬе М. 1. Т.

Ргевв, СагаЬг!63е, Мавв., 1968. БОБРОВ(ВОВКОТЧ Р.) 1964а Хайга! Ьапдиане !при! 1ог а Согарйег РгаЫегп-Бо)Ып3 БуЫегп, Рос(ога! Р!ввег(аБоп, МаввасЬивеКв 1пв1!(и(е о1 ТесЬпо1обу. См. также М, М1пвуу (ей), «БетапБс 1п(оппаБоп Ргосеяв!п8», ТЬе М. 1. Т. Ргевв, СагпЬг!63е, Маяв, 1968. 1964б А Яиейюп-Апвмег!п8 Був(егп (ог Н19ЫБсЬоо! А13еЬга %огд РгоЫегпв, 1п Ргос.

АР1РБ Ра!1 Лога! Согпри1ег Соп1., 591 — 614. БОЛЛ (ВАЬЬ %.) 1931 Майегпаг!са! КесгеаБопя апд Евваув, 101Ь ед., МасппВап апд Со., !Лй., Ьопдоп. (!5-ригг!е, рр. 224 — 228; Тоьчег-о(-НапаЬ рр 228 — 229.) ВАЙССМАН (ТЧЕ!ББМАХ С.) 1967 1.!БР 1.5 Рг!гпег, Р1с!гепвоп РиЫ!вЫп6 Согарапу, 1пс., Ве!гпоп(, Са!Д. ВОС, КАРСОН, РОБИНСОН (У«ОБ Ь., САКБОХ Р., КОВ!ХБОХ О.) 1964 ТЬе ()и!! Рге(егепсе Б!га(ебу !и ТЬеогега Ргоч1п6, Ргос. АР!РБ 1964 Ра!1 Яо1п! Согари1ег Сап1„чо! 26, рр.

616 — 621. ВОС, РОБИНСОН, КАРСОН (УУОБ Ь., КОВ!ХБОХ О., САКБОХ Р.) 1965 ЕНгс!епсу апб Сотр!е(епевв о1 йе Бе1 о1 Биррог( Б!га(е87 1п ТЬеогет-Ргоч!п3, Х. АСМ, 12, Хо. 4, 536 — 541. ГАРВЕИ, КЛИНГ (ОАКЧЕУ Т., КЫХО К.) !969 !!вег'в ОиЫе 1о РАЗ.5 Оиев(!оп-Апвьчег!п6 Був!егп, 51ап(огд КезеагсЬ !пьйи1е АгББс(а! !п(ейбепсе Огоир ТесЬп!са! Хо1е 15. ГАРД н др. (ОЫАКР 3.

е1 а1.) 1969 Бега!-Аи1огаа1еб МайегааБсв, Х. АСМ, 18, Хо. 1, 49 — 62. ГАРДНЕР (ОАКРХЕК М.) 1959 ТЬе Бс1епБВс Агпег!сап ВооЬ о1 МайегааБса! Ригг1ев апд Р!чегЫопв, Б!пюп апб БсЬив1ег, Хечч Уог1г. 1961 ТЬе Бесопд Бс!еп1!Пс Агпег!сап ВоаЬ о1 МайегааБса) Ригг1ев апов Р!четв!опв, Б!пюп апд БсЬиЫег, Хе~ч уог1с. 1961. 1964, 1965а, б, в МайегааВса! Оагаев, Бсб Ааь, 210, Хо. 2, 122 — 130 (РеЬгиагу 1964); 212, Хо. 3, 112 — 117 (МагсЬ 1965); 212, Хо.

6, 120 — 124 (Липе 1965); 213, Хо. 3, 222 — 236 (Бер1егаЬег 1965). ГЕЛЕРНТЕР (ОЕЬЕКХТЕК Н.) 1969 КеаБгаБоп о1 а Оеогпе(гу ТЬеогет-РгоЫп6 МасЫпе, Ргос. 1п1егп. Соп1. 1п1опп. Ргос., рр. 273 — 282, !!ХЕБСО Ноиве, Раг1в. См. также Фейген. баум Э., Фельдман Дж. (1963), стр, !45 — 164. ГЕЛЕРНТЕР, ХАНСЕН, ЛАВЛЕНД (ОЕЬЕКХТЕК Н., НАХБЕ~Х 3., ЬОЧЕ- 1.АХР Р.) 1960 Епьп(г!са! Ехр1огаБопв о1 йе Оеогпеггу ТЬеогегп Ргоч(пб МасЫпе, Ргос. Туев(. чогп! Согпри1ег Соп1., чо!.