автореферат диссертации по философии, специальность ВАК РФ 09.00.07
диссертация на тему:
Методологические основы логического программирования

  • Год: 1991
  • Автор научной работы: Фам Динь Нгьем
  • Ученая cтепень: кандидата философских наук
  • Место защиты диссертации: Москва
  • Код cпециальности ВАК: 09.00.07
Автореферат по философии на тему 'Методологические основы логического программирования'

Полный текст автореферата диссертации по теме "Методологические основы логического программирования"

л ч :• 9 ?

МОСКОВСКИ.! ОРДЕНА ЛЕНИНА ОРДЕНА ОКТЯБРЬСКОЛ РЕЗОЛЮЦИИ И ОРДЕНА ТРУДОВОГО КРАСНОГО ЗНАМЕНИ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ имени М.З. ЛОМОНОСОВА

Специализированный совет /Д 053.05.20/ по философским наукам при МГУ

На правах рукописи УДК 1 ми

?АМ ДИНЬ НГЬЕМ

/

:.Г';Т0Д0Л0ГИЧЕСК/М 0С;КШ ЛОГИЧЕСКОГО 1Ш0ГРААЬЫР0ВАНИЯ /АНАЛИЗ НА ОСНОВЕ Р^ТЕВАНГНОл ЛОГИКИ/

09.00.0? - Логика

Автореферат диссертации на соискание ученой степени кандидата Философских наук

Москва - 1991

Диссертация выполнена на кафедре логики философского факультета Московского государственного университета имени М.В. Ломоносова.

Научный руководитель:

доктор философских наук, профессор Смирнов В.А. Официальные оппоненты:

доктор философских наук, профессор Сидоренко Ё.А., кандидат философских наук, старщий научный сотрудник Стеблецова В.Н.

Ведущая организация - Всесоюзный научно-исследовательский институт системных исследований, отдел философских и социологических проблем системных исследований. Защита состоится 1991 г. в ... часов

на заседании специализированного совета /Д 053.05.20/ по философским наукам при Московском государственном университете им. М.В. Ломоносова, по адресу: Москва, Ленинские горы, 1-й корпус гуманитарных факультетов МГУ, философский факультет, 11 этаж, аудитория 1157.

С диссертацией можно ознакомиться в читальном зале 1-го корпуса гуманитарных факультетов МГУ.

Автореферат разослан "..." ....... 1991 г.

Ученый секретарь ^ ^ ,

специализированного совета Бочаров

.л : • ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Языки программирования, созданные в русле этого направления, принципиально отличаются от традиционных. Последние являются языками процедурного типа, т.е. составлая программы на этих языках, программист должен подробно описывать все шаги вычисления. Новые же языки заставляют программиста описывать ситуации и формулировать задачи, вместо того чтобы во всех деталях указывать способы решения этих задач. Система же будет решать заданные ей задачи. Ясно, что языки подобного типа представляют очень большой интерес для развития исследований в области исскуственного интеллекта, экспертных систем и информатики.

Цель работы. Основной целью нашего диссертационного исследования является выявление методологических основ логического программирования, строящегося на базе релевантной логики.

Задачи исследования:

- Проанализировать главные подходы к построению семантики логических прогоа'лч и сами эти семантики.

- Построить релевантную семантику общих логических прог-памм и применить ее к исследованию эквивалентности этих программ.

- Построить релевантную семантику расширенных программ.

- Показать, каким образом логические программы можно расс-

1

матривать как информационные состояния в смысле Белнала .

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

Методологической основой исследования являются диалектико-материалистические положения, согласно которым научные теории представляют собой определенные ступени познания мира и каждая научная теория базируется на определенных философских и методологических основаниях и предпосылках, которые могут быть применимы только к той области, где эти предпосылки имеют место.

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

Научная новизна работы. Основными результатами диссертационной работы являются:

- построена релевантная семантика неподвижных точек общих программ[ доказана теорема о соответствии этой семантики теоретико-модельной семантике этих программ,

- выявлены критерии, по которым можно заключить о различных типах эквивалентности общих логических программ,

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

-1

* См. Белнап Н. "Как нужно рассувдать компьютеру" // Белнап Н., Стил Т. Логика вопросов и ответов, М.,1981, с.208-209.

гических систем, в частности тенарного отношения достижимости между возможными мирами,

- построена релевантная семантика неподвижных точек расширенных программ, доказана теорема о соответствии этой семантики теооетико-модельно"' семантике этих программ,

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

- описана процедура вычисления для определенного класса расширенных программ, соответствующая построенно'* релевантно семантике этих программ.

Практическая значимость работы. Результаты исслодочаннн могут быть применимы для создания и совершенствования новых конструкций в языках логического программирования. ¡оедстазденные в диссертации результаты могут быть испочьзозаны и при чтении спецкурсов по релевантной логике и сст^и^е- ¿степсе.

Апробация работы. Результат'-! исследований по те?,га диссертации докладывались и обсундались на теоретическом семинаре кафедры логики "ялосо7ского "зкультета :.1Г/.

.'.о теме длссеотацш отубликованн лве печатные работы.

■Объем и структура работы. Дхссе^тацкя язлоязна на 1ЧР страницах машинописного текста. Она состоит из введения, трех глав '10 чатдгра'оз/, заключения и стшскп литературы. Список литературы включает 100 наименовали ' нг русском ч английском языках.

С0д2Р,ШШ РАБОТ"!

Зо зведении обосновывается актуальность теми, определяются цель и задачи исследования, определяются методологические и тео-

ретические основы работы, раскрываются научная новизна и практическая значимость работы.

В первой главе. "Современны^ направления семантических исследований логического программирования", даются предварительные сведения и анализируются основные современные направления семантических исследований логического программирования.

В §1, "Синтасис. Предварительные сведения", определяются основные понятия и рассматривается, семантика логических программ. В этом разделе определяются понятия подстановки, основной подстановки, непрерывной функции, неподвижной функции, программ, общих программ, расширенных программ, замыкания ррограммы и ряд других понятий. При этом автор приводит примеру ^помогающие лучше понять смысл определяемых здесь понятий. Далее рассматриваются семантики программ: теоретико-модельная семантика, семантика неподвижных точек, процедурная семантика. Приведены основные теоремы о свойствах программ, доказанные исследователями логического программирования.

Во втором параграфе, "Семантические исследования общих и расширенных программ", анализируются различные семантические подходы к исследованию общих и расширенных программ.- Кратко рассматриваются подход Габбая и Шергота, согласно которым отрицание можно трактовать как противоречивость, подход Маккарти, согласно которому отрицание понимается в интуицианистском смысле, а также подход Кларка и других, предлагавших использовать правило вычисления: "отрицание как неудача".

Автор перечисляет далее ряд сложных проблем, связанных с расширением выразительных средств "Пролога". Зот некоторые из них:

1. Логически эквивалентные программы могут иметь логически не эквивалентные замыкания.

2. Некоторые непротиворечивые программы имеют противоречивые замыкания. Например, программа

Р = {ДСаО 1 Я-СйО 3 непротиворечива. Но ее замыкание

Ссуу^Р (р) = [Ух-СйСхО А- и £в

содержит в себе формулу (^(л-) следовательно, проти-

воречиво .

3. Если Р есть общая или расширенная программа, а Тр -обобщение функции Тр, описанной в §1, то функция Тр немонотона, и поэтому нельзя построить семантику неподвижных точек для общих и расширенных программ.

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

Во второй главе. "Релевантная семантика общих программ", совершаэ-тся построение семантики /релевантной/ общих программ и исследуется вопрос об эквивалентности общих программ.

В первом параграфе, "Определения", на базе релевантной логики задаются необходимые понятия. Интерпретация здесь определяется как любое подмножество множества всех отмеченных формул языка. Отмеченная формула - это любое выражение вида ТХ или РХ, где Т л Р - два новых символа, которые интуитивно представляют "истину" и "лояь", а X - формула. Понятие выполнимости формул в интерпретациях определяется следующим образом:

2.3.1. Для пропозициональной переменной p¿

I И ?1 & Тр* е I , I № е Г

2.3.2. 1Н А ¿'В ^ X И А и Х>- В

А ^В ^ I ^ А ш 1 В

2.3.3. 1)= А УЗ I И А или I И- В I М- А V В I А и I И6 3 .

2.3.4. Г И 1А I ^ А Г ^ 7А Г^А

2.3.5. Для А и В, не• содержащих знака " ", 1Н(А =# В)

если I Н» А, то X Н В и если I Ь4 В то I М А.

. 2.3.6. Г И \/хА(х)для всякой орновной подстановки в , Г N , где 9*- ограничение в на переменную х.

2.3.7. X НЗхА(х) для некоторой основной подстановки 9> I 1= А 0х , где 5х- ограничение (9 на х. 1^3хА(х) <Н> для всякой основной подстановки в , 1 У" АОт*", где ограничение & на переменную х.

2.3.8. 1^1, X И3 1Л-, где - символ языка, который обозначает абсурд.

Интерпретация I выполняет множество формул V/ если I выполняет любой элемент \л/ .

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

в себе все логическое содержание программы Р и ничего больше. Интерпретация называется моделью С-ОУУьр (Р) , если она выполня-

ет Сауу^р (Р). Ассоциатируемый с программой Р трансформатор Фр определяется следующим образом:

Для произвольного основного атома А

ТА € ^рСг) тогда и только тогда, когда существуют правило Я В^,..., Зу^ в программе Р и основная подстановка 9 , такие, что = А и

11= з^е ¿г..., ¿6 .

РА (: ър(.Х) тогда и только тогда, когда для всякого правила X 3^,..., 3^ в программе Р и всякой основной подстановки 9 , таких, что = А,

I з^ и... & з^в .

Автор подчеркивает, что трансформатор Фр соответствует од-ноиаговому выводу основных атомов и их отрицаний из основных атомов и их отрицаний с использованием программы Р.

Доказывается теорема о том, что множество всех неподвижных точек трансформатора Фр ( РРСФ непусто и система { Р? ,с) представляет собой полную решетку. Более того, если обозначить наименьшую неподвижную точку трансформатора 5 через (Ч^), то имеет место: (Фр) = С[ \ I : I = Ф (Г)^ = ^рТ" .

Доказывается также теорема о соответствии между теоретико-модельной семантикой обших программ и семантикой неподвижных точек этих программ: Если интерпретация X выполняет теорию равенства Е<ц , то I является моделью замыкания программы Р тогда и только тогда, когда I является неподвижной точкой трансформатора Фр. Отмечается, что можно рассматривать так заданную семантику как семантику, построенную на основе четырехзначной логики Белнапа. Отмечается также, что построенная семантика отличается от семантики Фиттинга тем, что у Фиттинга не допускаются проти-

воречивые интерпретации, тогда как в этой семантике такие интерпретации допускаются. В конце параграфа констатируется, что программу можно представить в виде некоторого информационного состояния в смысле Белнапа, где начальное эпистемическое состояние состоит из одного единственного сетапа, являющегося наименьшим из сетапов, в которых "по крайней мере истинны" все факты программы, а правила представить формулами вида

Ухг...Ухл( ^.....х^) <Ы E1 V ... V Ei) из замыкания программы. Данные правила, будучи применимы к начальному эпистемическому состоянию, преобразуют его в новое эпистемическое состояние, состоящее из единственного сетапа, который может отождествляться с р) •

3 третьем параграфе, "Эквивалентности программ", исследуется вопрос об эквивалентности общих программ, Для этого используется трансформатор Фр. Вслед за Мейером, автор определяет функцию, соответствующую выводу с любым числом шагов ^Р] следующим образом:

[р](х) = Л ( 0Р +- IJ)1(X), где Id Ос) = X для всех X и (/ + f) (l) = /(x)U^(x).

'/'сследует вопрос о том, какие программы Р^ и удовлетворяет одному или нескольким из следующих условий:

1.5 = б рг ~Р2

2. ^ + 14 = %2 + Ы

3. = [г2]

С помощью ряда лемм доказываются следующие теореш:

2.4. Программа Р^ заменимо-эквивалентна программе Р., тогда

и только тогда, когда = i> .

Pi Р2

2.5. Пусть Р* и Р0 - программы. Тогда hid = i>_ + Т4

- 1 - 2

если и только если выполняется по кта":нэ;; мере одно из ело дующих у слови "г:

а. Зсе правила в Р, и PQ т-т-тоют вид 3 4= 3,

б. Зсе правила в п??еют литг 3 3 и дня всякого птлила С^ из Р^ существует правило С,; из Р9 такое, что vos-.eT заменить C.¿. -¡ли все наоборот.

в. и Р.; заченгота-экзиаалонтны.

Для исследования равенства [ Р- ] = Г3-?} вводятся :юв'п понятия. 0 помочью этих нов'« понята7 гоказнзоэтоя тоо^т'а:

Z.k. = [ ро ] тогда и только тогла, »» >•> w ■<•-

с я по wr- нэ'- ере одно ия слзду vrmx узловп;'.-

а. п 1)р состоят из правая з::да 3 <=* i,

б. состой, из ппавхл В'тда .1 и для всякого япазюга С^ из ?* оукоотвует правило из талое, что С^мсгсот зт'?нкть С9. /или все наоборот.

в. РГ ч Ро зам'Ш1тмо-эквиваи9нтнм.

1- а,

3 третье!' главе. "Релевантная семантика расширенных прогоа^л" осуществляется построение релевантно'* семантктж непоч.вгичх точек распярэянкх прогршлч на основе определенного истолкования молельных структур в лормальнчх семипчосах релевантных лог''к, а тажчэ показнвезтея, как можно рассматривать программу ктс "'н~ор-мационное состояние в смысле иелнапа.

3 первом параграге, "Семантика системы ^й.", внесено чг которое изменение з язык ££ . Гепеоь множество основных тоту/о.з конечное, но оно определяется так, чтобы их хватило для :г.—'с"-ш'я любого программы и любого запроса.

лонстатируется, что для составления программ и зат ■ всегда требуется конечное множество тертав, следоватечьло, :•>.••

- Vi -

ограничение на множество термов не влияет на семантику программ. Такое ограничение введено для того, чтобы стандартное определение квантора всеобщности, согласно которому VxA(.x) эквивалентно конъюнции АО*.,) & АСЛг).. где а-л, ... -все основные термы языка, соответствовало формализации этого квантора в аксиоматической системе Ей.

Далее излагается семантика системы ¿й , которая получается

1

из семантики системы 2, построенной Л. Л. Максимовой , прибавлением условий приписывания истинностных значений кванторным формулам в возможных мирах. Эти условия таковы:

ТО^сАс*))/^ Ум-С * HU ¿, ТС А*-'")/*.), Т( Эх А (*.))/ о~ 4=*- 31л. ( и 6

Формула А истинна в модельной структуре ^ К, Р, R, , ц) если ТА/а, для всякого мира а. из Р. Формула, истинная во всех модельных структурах, называется общезначимой формулой. Здесь и в дальнейшем ТА/а, есть сокращение для f (А, си) = Т, а ITA /а. ~ для q(А, а.) = не-Т.

Отмечается, что имеет место теорема о полноте и непротиворечивости системы Ей относительно изложенной семантики.

Зо втором параграфе, "Роль модельных структур в определении отношения логического следования. Характерная модельная структура", анализируется роль модельных структур в определении отношения логического следования. Диссертант показывает, что положение: "Если бывает случай, когда А истинно и В не истинно, то

А

•См. Максимова Л.Л. Структура с импликацией // Алгебра и логика, 1973, Т.12, 's4., а также Войшвилло ^.К. Философско-методоло-гические аспекты релевантной логики. М., 1988.

неверно, что из А следует В" вполне хватает для определения отношения логического следования, если следующее условие имеет место: "Если из А не следует В, то.всегда найдется случай, когда А истинно и В не истинно". Из этого автор делает вывод о том, что если применять множество возможных миров для определения отношения логического следования, причем для этого использовать только указанное выше положение "если бывает случай, когда А истинно и 3 не истинно, то неверно, что из А следует 3", то необходимо допустить ненормальные нормальные миры. Точнее: можно определить

АН 3 Уа^ТА/л. ТВ/а.) ,

если и только если множество всех миров удовлетворяет следующим условиям:

61. Для всякого высказывания А существует мир л., такой, что ТА/а. .

62. Для всякого высказывания А существует мир а. , такой, что не-ГА/ а, .

Далее в работе выясняется сущность тенарного отношения между мирами, используемого в формальных семантиках релевантных систем. Автор начинает с рассмотрения проблемы определения истинностного значения формул в возможных мирах. Особое внимание обращается на решение этой проблемы для формул вида А —» В. Подчеркивается, что если в мире я. высказывание А не истинно или высказывание 3 истинно, то в самом мире а. нет средств, с помощью которых можно решить рассматриваемую проблему. В силу этого обстоятельства необходимо для решения проблемы в мире а. рассмотреть некоторые "вспомогательные миры" Ьл и такие, что первый отличается от мира о. не больше, чем ТА/Ь< , а второй - не боль-

ше, чем не-ТЗ/Ьг, . Если Яр^аЬ обозначает, что Ь является "вспомогательным миром" для решения проблемы определения истинностного значения Формулы Л —» 3 в мире л. , то сказанное выше приведет к определению:

т(а —* в)/л. ^(ндв^и. (тал —> тз/О) .

Рассматривая особый случай формулы вида А —* 3, формулу зида А—»А, автор показывает, что для определения истинностного значения Формул этого вида и вообще для формул, главный знак которых есть знак импликации, в консеквент и антецедент которых входит некоторая одна и та же подформула, кроме вспомогательных миров Ц и , о которых шла речь выше, необходимо ввести и вспомогательный мир с , который может отличаться от и более чем независимым определением истинностного значения формулы А по сравнению с ее истинностными оценками в Ц или . Это положение разъясняется следующим образом. Мы используем метаязык для изучения объектного языка. При этом мы не хотим, чтобы метаязык мешал установлению законов объектного языка. Такое "вмешательство" проявляется в приписывании теории объектного языка законов метаязыка. Например, если мы приписываем второму вхождению А в А —>А значение "истинно" или "не истинно" только исходя из того, что первое вхождение А в А—»А имеет это значение, то на самом деле мы уже приписали теории объектного языка закон тождества метаязыка. Следовательно, необходимо устанавливать истинностное значение первого вхождения А в А—»А вне зависимости от истинностного значения второго вхождения А в А—»А и наоборот. Чтобы такое требование было выполнено, мы нуждаемся во

"вспомогательном мире" о , о котором шла речь.

в

Тенарное отношение между мирами Еда определяется теперь

следующим образом:

Я^аЛс 5АВЬс .

где ¿дозначает, что с может отличаться от ^ тем, что в нем истинностное значение А /или В/ установлено вне зависимости от истинностного значения А /или В/ в Ь , и не более, а Кдд«^ - это введенное выше бинарное отношение достижимости.

Таким образом, определение истинностного значения высказывания вида А —*В в мире л. уточняется следующим образом:

т(а-»в)/л <-=>^ ^^(к^оьс (та/ь ^ тз/<0).

Далее рассматривается проблема определения истинностного значения Формул вида 7А в возможных мирах. Очевидно, что если истинностное значение формулы вида ТА определяется в мире л. в зависимости от истинностного значения Формулы А в этом же мире, то только что установленное условие о независимых оценках тем самым нарушается. Следовательно, истинностное значение формулы 7А должно определяться вне зависимости от истинностного значения .формулы А в том же самом мире. Для этого используется вспомогательный мир л.*". Мир л* должен, с одной стороны, различать неистинность формул з мире а- от истинности отрицания этих Формул в этом же мире, а с другой - мир я? позволяет сохранить наше естественное понимание истинности 7 А как неистинности А. Определение 7А будет выглядеть теперь так:

Т7А/л. <н> 1 ТА/аГ .

Далее в диссертации исследуется понятие модельной структуры. На первый взгляд представляется, что приведенное выше определение импликации бесполезно для построения семантики следования, так как невозможно для каждой пары высказываний А и В языка ££ определить отношение Кдп. Автор решает эту трудность пу-

тем использования техники модельных структур. Действительно, вместо того, чтобы говорить о паре высказываний А и 3, можно ввести некоторую модельную структуру - пятерку (К, Р, Л, * где К - некоторое множество, Р £ К, Л- тенарное отношение на К, - функция из Ф X К, где V - множество формул языка, в множество \'Г, не-Т ] , * - унарная операция на К. Если теперь для каждой пары формул А и В существует модельная структура ^ К, Р, Я, , такая, что существует биективное отображение

о

из множества троек К в множество троек или существует биективное отображение из Я в Я^Ь'л, где йдз|М означает ограничение на множестве возможных миров, существенных для решения проблемы определения истинностного значения формулы А —»В, то имеет место определение:

3 модельной структуре V = ( К, Р, Я, Р, У ) Т(А-> В)/л. ¿Н с/у V^ (ТА/& => ТВ/с)). 3 этом определении отношение В. непосредственно уже не зависит от конкретной формулы А 3. Однако именно поэтому и становится необходимо упомянуть модельную структуру У . ¡.¡сдельная структура, таким образом, нужна для определения истинностных значений формул вида А—»3 в возможных мирах.

¡■.'¡одельная структура, соответствующая формуле Б, называется характерной модельной структурой /ХыС/ для Б. Пусть 'Ж. - семейство всех модельных структур. Тогда вполне возможно, что в "Ж входят, кроме модельных структур, характеризующих те или иные Тормулы, и модельные структуры, которые не характеризуют никаких формул. Конечно, при этом последние модельные структуры должны быть "нейтральными" по отношению к определению истинностных значений 1ормул а возможных мирах, т.е. они не должны отвергать

общезначимость Формул, которые истинны в характеризующих их модельных структурах. Аналогично, характерная модельная структура для формул ^ не должна отвергать общезначимость формулы Бо. общезначимость которой ее характерная модчльная структура не отвергает. Такие условия выполняются в силу выполнения условий, налагаемых на модельные структуры. Из всего этого понятно, что в определении импликации в модельной структуре можно опускать упоминание о самой модельной структуре, так как отстающая часть предложения касается только ХМС для формулы, о которой идет речь в этом определении. 3 результате:

3 любой модельной структуре

Г (А—* з)/ я. ¿Н^ ^ (ТА/Ь <Ч> ТЗ/с)) .

3 работе далее исследуются условия, удовлетворяя которым структура становится модельной, т.е. ограничения, накладываемые на К, Р, Я, * , ц> . Доказывается, что все постулаты семантики системы Е являются следствиями вышеуказанных условий. Доказывается теорема о том, что множество всех модельных структур, установленных автором, является подмножеством множества всех модельных структур в семантике системы Е. Это означает, что система Е и система Ей Формализуют некоторые понимания отношения логического следования. Это дает право считать, что изложенные з параграфе рассуждения о модельных структурах вполне применимы к модельным структурам построенной Л.Л. Максимовой формальной семантики системы Е.

3 третьем параграфе, "Семантика неподвижных точек", совершается построение семантики неподвижных точек расширенных программ. Семантика построена на основе двух трансформаторов Тр и <!>, которые определяются следующим образом:

Пусть даны модельная структура ¡Г и программа Р. Тогда:

Тр: К 5>(к),

Ь 6 ТрОО тогда и только тогда, когда для всякого основного атома А верно:

ТА/Ь , если и только если существует в программе Р правило К. £[_,..., и существует основная подстановка 9- , такая, что И6 = А и сО= ¡^ & .

Т7А/ь , если и только если для всех основных подстановок В и для всякого правила Н. %..........в Р, та-

ких, что 5.6 = А, <*-№ К^ Яу^в .

г

Пусть Т^К, тогда а. е Фр(1) если и только если а. е J к

а е трс<0 .

Доказывается теорема:

(фр) = [ Л : л е ТрСл-Я = Ы: л. N

Отмечается, что ¿^»(фр) в построенной семантике играет аналогичную роль, какую играет (фр) в семантике для общих программ в гл. 2.

В конце параграфа приведены определения, которые, по мнению автора, должны служить для целей исследования вопросов о полноте и непротиворечивости процедур вычисления относительно построенной семантики.

В четвертом параграфе, "Программа как информационное состояние", автор показывает, что программу можно представить в виде информационного состояния в смысле Белнапа. Подчеркивается, что здесь, в отличие от Белнапа, допускаются правила вида А —»В, где А и В - любые, не содержащие знак "=■>", бескванторные Формулы. В силу этого, изложенная концепция информационного состоя-

ния представляет собой определенную модификацию аналогичной концепции Белнапа. Введены понятия эпистемического состояния, информационного состояния и некоторые другие. Автор показывает, что программу Р может быть рассмотрена как информационное состояние , е) , где Е - эпистемическое состояние, Е = {а-: ТА/«? для всех фатов программы Р, как позитивных, так и негативных, а

- множество формул вида Ух^... Ух„(и(х^,... ,х^)<4-> Е^и... V Е^ из р). Доказывается теорема о том, что если (£, , Е )> - со-

поставимое с программой Р информационное состояние, то результат применения £ к Е есть не что иное, как ^/^(Фр). т.е. множество всех выполняющих СетрСр) миров.

В последнем, пятом, параграфе, "Процедура вычисления для расширенных программ", кратко описывается процедура вычисления для определенного класса расширенных программ. Эта процедура представляет собой расширение изложенной в §2 гл. 1 процедуры ОЕР Кларка.

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

Основное содержание диссертации отражено'в следующих публикациях автора:

1. Релевантная семантика логического программирования // Неклассическая логика и компьютерная наука /Труды научно-исследовательского семинара сектора логики Института философии

АН СССР/./З печати/.

2. Релевантная семантика логического программирования. 2.// Логические исследования, т.2 /В печати/.