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

САНКТ-ПЕТЕРБУРГСКИИ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи

Ашраф Абд Эль-Фаттах Мустафа Дарвиш

РАСШИРЕНИЕ ПРЕДИКАТНЫХ ФОРМУЛ ЛИНЕЙНЫМИ НЕРАВЕНСТВАМИ И СПИСКАМИ ДЛЯ СПЕЦИФИКАЦИИ ПРОГРАММ

()5.13.17-Теоретические основы информатики

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург 2006

Работа выполнена на кафедре информатики математико-механического факультета Санкт-Петербургского государственного университета.

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

Косовский Николай Кириллович

Официальные оппоненты: доктор физико-математических наук,профессор

Братчиков Игорь Леонидович;

кандидат технических наук,доцент Керов Леонид Александрович

Ведущая организация: Санкт-Петербургский институт информатики

и автоматизации, Российской Академии Наук

Зашита диссертации состоится « . 2006 г. в Ж Ч2&.00 МИН.

на заседании диссертационного совета Д 212.232.51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу: 198504, Санкт-Петербург, Петродворец, Университетский проспект, д.28. Математико-механический факультет Санкт-Петербургского государственного университета.

С диссертацией можно ознакомиться в Научной библиотеке Санкт-Петербургского государственного университета по адресу: 199034, Санкт-Петербург,Университетская набережная, д.7/9.

Автореферат разослан «. /¿7 » О Я 2006 г.

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

диссертационного совета Д 212.232.51, доктор физико-математических наук,

профессор ДЙ^мКбИ1«* Б.КМартыненко

¿ШР6А-

Актуальность темы

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

Задача создания формализованного языка для доказательств правильности программ являет собой сердце современной компьютерной науки [13]. В диссертации представлена расширенная логика высказываний с дополнительными линейными неравенствами пропозициональных формул и принадлежностью значения линейной комбинации пропозициональных формул списку их значений. Также представлено секвенциальное исчисление, соответствующее такой логике. Предложенное в диссертации секвенциальное исчисление может быть использовано для представления знаний в информационных системах.Переход от исчислений гильбертовского типа к секвенциальным прослеживается, например, в [8]. Предложенные в этой логике расширенные формулы также более удобны для описания реализации идеи перцептрона и других нейронных сетей [9,15,20]. Имеются приложения нейронных сетей в медицине,например [16].

Основополагающим инструментом исследователей искусственного интеллекта является представление знаний, которое сводится к задаче разработки формального языка, подходящего для спецификации компьютерных программ. В этой диссертации разработаны важные средства расширения предикатной логики первого порядка, как формального языка для описания свойств и отношений между объектами. Язык, который разработан, также может быть использован в расширенных математических формулах для написания спецификаций программ, использующих типы короткого целого числа, целого числа и длинного целого числа.Предлагаемый расширенный язык может использовать метрику Хэмминга,сохраняя линейный характер исходных предикатов в отличие от [19], где используется эвклидова метрика.

МакДермотт [14] и другие считают,что ключ к написанию успешной программы, основанной на знаниях, заключается в выборе правильных инструментов представления знаний. Предикатная логика первого порядка предлагает много инструментов, которые важны при решении задач искусственного интеллекта. Имеются приложения в экономике,например [18].

В этой работе представлена новая логическая связка, которая называется линейным неравенством. Эта связка удобна для построения экспертных систем на языке Пролог.

Основываясь на этой логической связке, была разработана экспертная система образовательной направленности для университета Хельван (Каир, Египет), предназначенная для того, чтобы давать рекомендации на разных этапах учёбы в университете.

Задача проверки правильности компьютерной программы связана с доказательством корректности программы. Одной из весомых иллюстраций практичности этой диссертации является то, что разработан в ней формальный язык спецификаций для доказательства корректности программ [17]. Такие инструменты, как .например, Java Modeling Language (JML) [12],возникли, чтобы помочь разработчикам более формально определить поведение компонент в больших системах. JML недостаточно формализован и основывается на традиционной логике, но в предложенном языке спецификаций использована расширенная логика, достаточная, как показано на примерах, для доказательства правильности учебных программ, написанных на языке Паскаль.

Цель работы

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

Многие варианты применения компьютеров сводятся к применению лишь конечных множеств рациональных чисел (из конечной области определения). В этой работе представлено расширение логики высказываний в виде секвенциального исчисления. Рациональные числа используются как коэффициенты линейных комбинаций.Определённое исчисление удобно применять при анализе и построении информационных систем.

Фрэнк Розенблатт вывел алгоритм обучения для сети, носящей имя «перцептрон». Входные значения и значения уровней активации - «1» или «-1»; причем веса являются вещественными числами. Предложенные в диссертации расширенные формулы более удобны для формализованного описания идеи «перцептрона» в нейронных сетях (см.также [9,15,20]).

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

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

Для разработчиков ПО важно не только понимать, что программа делает во всех случаях, но и иметь возможность это доказать.Имеется в виду, что, если кто -то представляет документацию относительно того, что программа должна делать, программист обязан доказать этому человеку,используя математические доводы, что программа и документация соответствуют друг другу.

Когда это сделано, программа может называться «правильной». Доказательство правильности программ аналогично доказательству теорем. Другими словами, программа полностью правильна, если она (заканчивая свою работу) удовлетворяет постусловию при всех входных значениях, удовлетворяющих предусловию [17]. Таким образом,разработан новый язык формализованных спецификаций, основанный на разработанной логике.

Научная новизна

В этой диссертации получены результаты, которые новы, важны и являются ключевыми в области представления знаний, особенно для описания (спецификации) систем ПО и их разработки. Произведено полезное и нетривиальное расширение логики высказываний (секвенциального исчисления).Рациональные числа были использованы в качестве коэффициентов линейных комбинаций. Доказано, что предложенное исчисление семантически обосновано и полно. Предложенное исчисление более удобно для использования,чем из [7], поскольку использует линейные комбинации,а не моделирование только суммы пропозициональных переменных.

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

В качестве иллюстрации была реализована экспертная система на языке программирования Пролог, предназначенная для того, чтобы сопровождать учебный процесс в университете Хельван (Каир, Египет). В этой системе были использованы линейные неравенства в качестве новой логической связки. Эта экспертная система может давать рекомендации студентам на разных этапах обучения.

Новая логика была использована для языка спецификаций, предназначенного для доказательства корректности на языке Паскаль для трех типов данных: integer, short integer и long integer.

В расширенном языке предикатов можно легко моделировать юнкцию из [4] и расширить предложенное исчисление, как в [2,3,11].

Инструменты, вроде JML (Java Modeling Language), появились, чтобы помочь специалистам более формально описывать поведение компонент в больших системах. JML основывается на традиционной логике, но предложенный в диссертации язык спецификаций использует расширенную логику.Заметим, что для предложенного языка спецификаций алгоритмически разрешима проблема проверки тождественной истинности формул для этого языка.

Основные результаты

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

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

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

(Каир, Египет).

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

Практическая и теоретическая ценность

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

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

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

В диссертации разработана и реализована экспертная система для образовательного процесса в университете Хельван (Каир, Египет).Эта система выдаёт рекомендации и советы по выбору специальности на разных этапах обучения (бакалавриат, магистратура, аспирантура, получение звания доцента).Она реализована на языке программирования Пролог.

Разработан новый язык спецификаций, основывающийся на расширенной логике первого порядка.Этот язык может быть использован для записи доказательств правильности многих программ, реализованных на языке Паскаль и представленных в [7]. Примеры спецификации ряда таких программ разработаны в диссертации.

Апробация работы

Основные результаты этой диссертации были представлены в трудах следующих конференций:

1. Современная логика, Проблемы теории, истории и применения в науке,Труды VIII Общероссийской научной конференции, 24-26 июля 2004, Санкт-Петербург.

2. The 8th World Multi-Conference on Systemics, Cybernetics and Informatics, http://www.iiisci.org/sci2004, July 18-21, 2004, Orland, Florida, USA.

3. The 1st World Congress and School on Universal Logic, http://www-uni-Iog. org, 26th March -3rd April, 2005, Montreux, Switzerland.

Публикации

Все основные результаты этой диссертации были опубликованы в изданиях на трех конференций в США, РФ и Швейцарии. Все публикации описаны в конце этого автореферата.

Структура и объем диссертации

Эта диссертация состоит из введения ,пяти глав, заключения и списка литературы. Текст диссертации написан на 128 стр. Список использованной литературы и публикаций состоит из 48 ссылок. Два приложения составляют 106 стр.

Содержание работы

Во введении обосновывается актуальность темы исследования,формулируются цели задачи работы. Рассказаны исторические истоки, относящиеся к этой работе. Представлено краткое описание структуры диссертации.

В первой главе собраны необходимые предварительные сведения

из [3].

Раздел 1 первой главы посвящён метаязыку (формализованное описание синтаксических понятий).

Раздел 2 посвящён определению пропозициональной формулы. В третьем разделе даны определения терма и предикатной формулы. Четвёртый раздел посвящён изложению секвенциального исчисления предикатов.

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

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

(i) Истина,ложь, пропозициональные переменные являются расширенными пропозициональными формулами.

(И) Если«,/? и S являются расширенными пропозициональными формулами и Lj,L2,...,Lk (к >2)-линейные комбинации расширенных пропозициональных формул, ТО (L,=L2), (=[L„...,Lk])(L, €[L2,...,LJ), (L, <;L2), (a&ß), (a => ß), (« <=> ß), —iQf, {awß) и {ifa then ß else 8 fi) также являются расширенными пропозициональными формулами.

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

определение секвенции, как слова, которое начинается со знака секвенции «-►» и состоит из списка формул (членов секвенции).

Интерпретация секвенции - дизъюнкция интерпретаций всех формул (членов секвенции). Интерпретацией секвенции, которая состоит только из одного знака секвенции, является -1 (ложь).

Определим, когда секвенция S является аксиомой. Сначала удалим все формулы, которые включают бинарные логические связки, кванторы и вложенные неравенства. После этого построим систему линейных неравенств следующим образом. Нечетное количество знаков логического отрицания перед формулой заменяем единственным арифметическим отрицанием, и четное количество отрицаний удаляем Затем меняем все неравенства вида (х -< у) на неравенства (у < х) и все неравенства вида (* < у) на (у<х) , где х, у - линейные комбинации пропозициональных переменных (логическое отрицание заменено одноместным минусом). Наконец,получаем систему неравенств из секвенции.

Секвенция S является аксиомой тогда и только тогда, когда полученная система линейных неравенств неразрешима в числах из множества {-1,1}. Например, секвенция -»(0 < Л)(0 s -Л) - аксиома предлагаемого исчисления.

Далее будем использовать прописные буквы для формул и Г для конечных списков формул. Исчисление имеет следующие правила:

• правило перестановки членов секвенции.

• правило для вложенных неравенств:

Вложенные неравенства типа (L, -<t2), (L, <L2) могут быть заменены на (if L\<L2 then 1 else -1 ft), (if A ^ ¿> then 1 else -1 fi) соответственно.

• правила отрицания в неравенствах

->T(L+B<L|+A) , . r(L+-iB<L, +А)

-> r(L+-iA<L, +-iB) T(L+-.A<L, +B)

>I-(L+A<L, +-.B)

-> Г(Ь+В<Ь, + -.А)

и эти же правила с заменой знака < на знак <,а также правила снятия и навешивания двойных отрицаний в равенствах и принадлежностях спискам.

• правила отрицания вне неравенств

Г->(А < В) ->Г-,(А<В)

-> ГА Г-i-iA

• правила для конъюнкции и дизъюнкции в неравенствах

->Г(1, +A<L + C)m + В < L + C)

->Г((Д +(A&B))<L + C) -Г (L + C<L,+A) -Г(Ь + С<Ц+В)

► Г(1 + С < Ц+(А& В)) -+Т(Ь + А<Ц +С) -»Г (I + Bci, +С)

► T((L + (Av В)) < ¿| +С)

► Г(1, +C<L + A){L, +C<L + B)

(v<),

(<v),

-*Г((1, +C<L + (AvB)) и эти же правила с заменой знака < на знак <, а также аналогичные правила для =>, <=>.

• правила для конъюнкции и дизъюнкции вне неравенств

-> ГА

(&) ^ГАВ (V)

Г(А&В) -> Г(А v В)

-> Г-iA

-> Г-iA-IB . .. ->Г-Я , .

- (-1 &) - (-, v)

r~i(A&B) Г->(А v В)

и аналогичные правила для =>, о и if then else.

• правила для условных выражении в неравенствах

► Г(В й A)(L, +D ^ L)

► r(A<BXL,+C<L)

• r(L,+if (В < A) then С else D fiSL)

► Г(В < AXL < L, +D)

► Г(А<В)(Ь < L|+C)

- Г(Ь < L, +if (В 5 A) then С else D fi)

-> Г(В < A)(L, +EKL) Г(А<В)(Ь, +C<L)

• T(L, +if (В < A) then С else D fi<L)

(if S),

(Sift

(if<),

> Г(В £ A)(L<L, +D) •r(A<B)(L<L,+C)

(<if).

-» r(L<L, +if (BiA) then С else D fi)

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

* правила для равенства

-*■ Г(Ь £ L,)

->r(L,<;L) ->r^(L^L,b(L,<L)

-»r(L=L,) ->r4L=L,) Л

"-¿-,' = 4) MIX =

' правила принадлежности

-Г ^(£,=1,)

• правила для списка с одним элементом

->г(Ъб[ь,])

• правило перемножения двух рациональных множителей с заменой их на результат перемножения.

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

Четвёртый раздел посвящен доказательствам некоторых теорем. Теорема 1 утверждает,что аксиомы и правила вывода предложенного секвенциального исчисления корректны в обычном понимании термина «секвенция» и арифметических знаков+.=,%<. В теореме 2 речь идёт об

обращении правил для предложенного секвенциального исчисления, а именно: обращение любого правила секвенциального исчисления является допустимым правилом. Полное доказательство находится в приложении к диссертации. Теорема 3 утверждает,что разрешимости: предложенное секвенциальное исчисление полно для тождественно истинных интерпретации расширенных пропозициональных формул.В конце главы доказано утверждение о NP-полноте задачи выполнимости расширенной *

пропозициональной формулы.

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

(i) Каждая атомарная формула является расширенной предикатной формулой.

(ii) Если а,р и S являются расширенными предикатными формулами и Ll,L1,...,Lk,{k>7) -линейные комбинации расширенных предикативных формул,то {Ц -с/,),(!, (=[£,,...,!,]),(£, е[£„.-.А» (А (« & Л.

(а => /?),(ао Р), -.а, (av(J)H (ifa then ¡5 else 6 fi) также являются расширенными предикатными формулами.

(iii) Если v - переменная, а а - формула, тогда 3va и Vvar также являются расширенными предикатными формулами.

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

В четвёртой главе представлена экспертная система, которая обслуживает образовательный процесс в университете Хельван (Каир, Египет), т.е. даёт рекомендации по выбору специализации.Вся база данных для этой части взята из информации по факультету естественных наук.Первый раздел этой главы относится к степени бакалавра, второй — магистра, третий - кандидата наук (Ph.D.), и , наконец , - доцента. В каждом разделе представлены основные курсы учебных дисциплин с отметками и перечислены разные случаи в различных ситуациях, затем представлены правила, основываясь на которых, даны рекомендации. В конце каждого раздела предъявлены некоторые цели программ системы (использующие соответствующие базы данных). Все эти подсистемы реализованы на языке *

Пролог.

Пятая глава посвящена предлагаемому языку спецификаций для записи утверждения о частичной корректности программ в целом [1]. В первом разделе представлено несколько базовых понятий и определений для языка спецификаций, включая обзор JML выражений В следующем разделе дано определение расширенного терма языка спецификаций, которое гласит:

(i) Каждая переменная для каждого типа данных является расширенным термом.

(ii) Если /,и t2- расширенные термы, то

(i, +/2),(/, ~t2),(t, *t2),(h div г2),(г, Лt2),(t!),Fib(t,)являются расширенными термами.

(iii) Если t -расширенный терм, то ^ t j - также расширенный терм.

(iv) Каждое число типа SHORTINT является термом и лежит в отрезке:

-32768...32767

(v) Каждое число типа INTEGER является термом и лежит в отрезке:

-2147483648...2147483647

(vi) Каждое число типа LONGINT также является термом и лежит в отрезке:

-9223372036854775808...9223372036854775807

(vii) Если х- переменная, a r,,/2,...,it-термы, то x[f,,i2,...,fj — терм.

(viii) Если х — переменная, тогда input [х], output [х] - термы.

Во втором разделе определена атомарная формула языка спецификаций и линейная комбинация строк. В этом же разделе дано определение формулы языка спецификаций следующим образом:

(i) Каждая атомарная формула является формулой языка спецификаций

(ii) Если L, М, N - формулы языка спецификаций, то

(i & М), (£ V M),(L=> M),(i« М), (if L then N else M ft) являются формулами языка спецификаций.

(iii) Если а,, а2.....а„,(и > 2)- линейные комбинации формул языка

спецификаций, то (а, =а2),(л, ^а2),(а, >а2),(=[а,,...,а„]),(а1 е[а2,...,«„]) -формулы языка спецификаций.

(v) Если V- переменная, а а - формула языка спецификаций, то 3 v а и V V а - также формулы языка спецификаций.

Разделы 3 и 4 посвящены использованию языка спецификаций для утверждений о корректности программ, описанию аксиом и правил вывода из [10]. В пятом разделе представлена основная задача этой главы:примеры утверждений о корректности программ на предложенном формальном языке спецификаций.Приведены примеры некоторых программ, реализованных на языке Паскаль из [7], с формализованными спецификациями,

обеспечивающими частичную корректность этих программ в целом [1] на предложенном языке спецификаций.

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

В приложении 1 и 2 излагаются дополнительные детали доказательства теоремы 2 из главы 2.

Список литературы

1. Косовский Н.К.,Элементы математической логики и ее приложения к теории субрекурсивных алгоритмов,Изд-во Ленинградского Университета, Ленинград, 1981.

2. Косовский Н.К., Уровневые логики, Записки научн.семинаров санкт-петербургского отделения математического института им.В.А.Стеклова, том 220,1995,с.72-82.

3. Косовский Н.К. и А.В.Тишков, Логики конечнозначных предикатов на основе неравенств, Изд-во Санкт-Петербургского Университета, Санкт-Петербург, 2000.

4. Тельпиз М.И,Представление булевых функций, Кибернетика, No.4, 1985, с.37-40.

5. Aho A.V., Ulman J.D., Foundations of computer science, Computer Science Press, New York, 1992.

6. Buss S., Clote P., Cutting planes, connectivity and threshold logic, Archive for Mathematical Logic, 35,1996, pp.33-62.

7. Dromey R.G., How to solve it by computer, Prentice Hall International Series in Computer Science, London, 1982.

8. Gabbay, M.Cheney, J., A sequent calculus for nominal logic, IEEE Symposium on logic in computer science, 13-17 July, 2004, France, pp.139-148.

9. Giorgio fumera, Fabio Roli, A theoretical and experimental analysis of linear combiners for multiple classifier systems, IEEE transactions on pattern analysis and machine intelligence, vol.27, No.6, June, 2005, pp.942-956.

10. Hoare C.A., An axiomatic basis of computer programming, Communications of the ACM, Vol.12, No. 10, 1969, pp. 567-580.

11. Kossovski N.K., Tishkov A.V., Logical theory of Post logic with linear order. // Technical Report TR-97-11. Department of Informatics, University Paris-12, Paris, 1997,9p.

12. Leavens Gary T., Baker Albert L., and Ruby Clyde, Preliminary design of JML: A behavioral interface specification language for

Java, Department of Computer Science, Iowa State University, December, 2004.

13. Luger F.G., Artificial intelligence, structures and strategies for complex problem solving, Addison-Wesley, Pearson Education, 2000.

14. McDermott D. and Doyle J., Non-monotonic logic l.In: Artificial Intelligence, No.13,1980, pp.14-72.

15. Park JW, Harley RG, Venayagamoorthy GK, Inelligent control of a synchronous generator using MLP/RBF neural networks and lyapunov transient stability analysis of the controllers, IEEE transactions on neural networks, Vol.15, No.2, March 2004, pp.460-464.

16. Roger Hult, Grey-Level morphology combined with an artificial neural networks aproach for multimodal segmentation of the hippocampus,The 12th International Conference on Image Analysis and Processing (ICIAP'03), IEEE, 2003, pp.277-282.

17. Slonneger K., Kurtz B L., Formal syntax and semantics of programming languages, Addison-Wesley, 1995.

18. TerSsvirta Timo, van Dijk Dick and Medeiros Marcelo, Linear models, smooth transition autoregressions, and neural networks for forecasting macroeconomic time series: A re-examination, International Journal of Forecasting, 2005, pp.755-774.

19.www.faqs.org/faqs/ai-faq/neural-nets/part2/sectioni.html, What are combination, activation, error, and htm, Part 2, January, 2006.

20. Yang Shuyuan, Wang Min and Jiao Licheng, A new adaptive ridgelet neural network, Advances in neural networks ISNN, Second International Symposium on Neural Networks, May 30-June 1, Chongqing, China, 2005, pp.385-390.

Работы автора по теме диссертации

1. Косовский Н.К., Дарвиш А.А.,Расширение пропозиционального секвенциального исчисления списками и сложением,Современная логика:проблемы,теории, истории и применения в науке, Материалы VIII Российской международной научной конференциии,24-26 июня 2004, Санкт-Петербург,2004,с.497- 499.

2. Kossovski N.K., Darwish А.А., Propositional Sequent Calculus with list Construction and Addition, The 8th World Multi-Conference on Systemic, Cybernetics and Informatics, July 18-21, Vol.1, Orlando, Florida, USA, 2004, pp.l7-19.

3. Kossovski N.K., Darwish A.A., Two Sequent Calculuses with Inequalities of Linear Combination, 1st World Congress and School on Universal Logic, 26th March-3rd April, Montreux, Switzerland, 2005, pp.61- 64.

Подписано в печать 03.02.2006 Формат 60x84 1/16.Бумага офсетная. Печать офсетная. Усл. печ. л. 1,0. Тираж 100 экз. Заказ №271

Отпечатано в ООО «Издательство "JIEMA"»

199004, Россия, Санкт-Петербург, В.О., Средний пр., д.24, тел./факс: 323-67-74 e-mail: izd_lema@mail.ru

ВВЕДЕНИЕ

ОГЛАВЛЕНИЕ

Глава1. Секвенциальное исчисление предикатов

§1.1. Метаязык для определения логических формул.и

§ 1.2. Определение пропозициональной формулы.

§ 1.3. Формальный аппарат выводимости.

§ 1.4. Язык исчисления предикатов.

§ 1.5. Секвенциальное исчисление предикатов.

Глава 2. Пропозициональное исчисление с неравенствами линейных комбинаций формул и принадлежностью значений таких комбинаций списку из них

§2.1. Введение.

§2.2. Определение пропозициональных формул,расширенных неравенствами линейных комбинаций и принадлежностью значений спискам из них.

§2.3. Аксиомы и правила вывода предлагаемого исчисления.

§2.4. Теоремы о расширенном исчислении высказываний.

Глава 3. Расширенное исчисление предикатов первого порядка бо

§3.1. Основные определения.

§3.2. Исчисление для расширенных предикатных формул.

§3.3. Допустимость правила сечения.

§3.4. Теоремы о свойствах исчисления.

Глава 4.Экспериментальная информационная система для образовательного процесса в Хелванском университете (Каир,Египет)

§4.1. Введение.

§4.2. Информационная система для выбора бакалаврской программы обучения.

§4.3. Информационная система для выбора магистерской программы обучения.

§4.4. Информационная система для степени кандидата наук

Ph.D) на отделении математики.

§4.5. Информационная система для получения звания доцента.

Глава 5. Формальный язык для проверки корректности программ на основе расширенных предикатных формул

§5.1. Введение и основные понятия.

§5.2. Определение языка спецификаций.ЮЗ

§5.3. Синтаксис утверждения о корректности программы.Ю

§5.4. Аксиоматический подход к корректности программ.

§5.5. Примеры корректных программ с использование предложенного формального языка спецификаций в комментариях.

Актуальность темы.Представление знаний является самым важным понятием, связанным с искусственным интеллектом, и имеет широкие приложения [32,33].

Для того чтобы преодолеть многие трудности в области разработки программного обеспечения (ПО) всё большее количество учёных обращается к символической логике, как средству описания программного продукта [20,31,38].

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

Задача создания формализованного языка для доказательств правильности программ являет собой сердце современной компьютерной науки.В диссертации представлена расширенная логика высказываний с дополнительными линейными неравенствами пропозициональных формул и принадлежностью значения линейной комбинации пропозициональных формул списку их значений. Также представлено секвенциальное исчисление, соответствующее такой логике.Предложенное в диссертации секвенциальное исчисление может быть использовано для представления знаний в информационных системах.Имеются приложения нейронных сетей в медицине ,например, [43].Предложенные в этой логике расширенные формулы также более удобны для описания реализации идеи перцептрона и других нейронных сетей [22,41,48].

Основополагающим инструментом исследователей искусственного интеллекта является представление знаний, которое сводится к задаче разработки формального языка, подходящего для спецификации компьютерных программ [33].В этой диссертации разработаны важные средства расширения предикатной логики первого порядка, как формального языка для описания свойств и отношений между объектами. Язык, который разработан, также может быть использован в расширенных математических формулах для написания спецификаций программ, использующих типы короткого целого числа, целого числа и длинного целого числа. Предлагаемый расширенный язык может использовать метрику Хэмминга,сохраняя линейный характер исходных предикатов в отличие от [47],где используется эвклидова метрика.

МакДермотт и другие [35] утверждали, что ключом к написанию успешной программы, основанной на знаниях, является выбор правильных инструментов представления знаний.Многие варианты применения искусственного интеллекта сводятся к использованию лишь конечных множеств рациональных чисел из конечной области определения.В этой работе разработано расширение логики высказываний и секвенциального исчисления для него. Использованы линейные неравенства, в которых рациональные числа используются как коэффициенты линейных комбинаций [6,29,30]. Переход от исчислений гильбертовского типа к секвенциальным прослеживается ,например,в [19].Так определённое исчисление в ряде случаев более удобно применять к анализу и созданию информационных систем,чем традиционную логику первого порядка. Имеются приложения в экономике,например,[46].

В этой работе представлена новая логическая связка, которая называется линейным неравенством. Эта связка удобна для построения экспертных систем на языке Пролог, использованного в [36].

Основываясь на этой логической связке, была разработана экспертная система образовательной направленности для университета Хельван (Каир,

Египет), предназначенная для того, чтобы давать рекомендации на разных этапах учёбы в университете.

Задача проверки правильности компьютерной программы связана с доказательством корректности программы. Одной из весомых иллюстраций практищности этой диссертации является то, что разработан в ней формальный язык спецификаций для доказательства корректности программ [25,45]. Такие инструменты, как, например, Java Modeling Language (JML) [29],возникли, чтобы помочь разработчикам более формально определить поведение компонент в больших системах.ХМЪ основывается на традиционной логике, но в предложенном языке спецификаций использована расширенная логика, достаточная, как показано на примерах,для доказательства правильности учебных программ, написанных на языке Паскаль [17].

Цель работы.В экспертных системах существует множество алгоритмов, основанных на математической логике (точнее - на предикатах) [30,42]. В этой работе представлена новая логическая связка, которая оказывается полезной в экспертных системах, когда требуется использовать представление суммарных знаний.

Многие варианты применения компьютеров сводятся к применению лишь конечных множеств рациональных чисел (из конечной области определения).В этой работе представлено расширение логики высказываний в виде секвенциального исчисления.Рациональные числа используются как коэффициенты линейных комбинаций.Определённое исчисление удобно применять при анализе и построении информационных систем [23,34].

Фрэнк Розенблатт предложил алгоритм обучения для сети, носящей имя «перцептрон». Входные значения и значения уровней активации - «1» или «-1»; причем веса являются вещественными числами .Предложенные в диссертации расширенные формулы более удобны для описания идеи «перцептрона» в нейронных сетях [22,41,48].

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

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

Для разработчиков ПО важно не только понимать, что программа делает во всех случаях, но и иметь возможность это доказать.Имеется в виду, что,если кто-то представляет документацию относительно того, что программа должна делать, программист обязан доказать этому человеку,используя математические доводы, что программа и документация соответствуют друг другу.

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

Научная новизна.В этой диссертации получены результаты, которые новы, важны и являются ключевыми в области представления знаний, особенно для описания (спецификации) систем ПО и их разработки.Произведено полезное и нетривиальное расширение логики высказываний (секвенциального исчисления). Рациональные числа были использованы в качестве коэффициентов линейных комбинаций. Доказано, что предложенное исчисление семантически обосновано и полно.Предложенное исчисление более удобно,чем предложенное в [14],где не используются линейные комбинации.

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

В качестве полезной иллюстрации была реализована экспертная система на языке программирования Пролог, предназначенная для того, чтобы сопровождать учебный процесс в университете Хельван (Каир, Египет).В этой системе были использованы линейные неравенства в качестве новой логической связки.Эта экспертная система может давать рекомендации студентам на разных этапах обучения.

Новая логика была использована для языка спецификаций, предназначенного для доказательства корректности на языке Паскаль [17] для трех типов данных: integer, short integer и long integer.

В расширенном языке предикатов можно легко моделировать юнкцию из [9] и расширить предложенное исчисление, как в [5,8,28].

Инструменты, вроде JML (Java Modeling Language),появились, чтобы помочь специалистам более формально описывать поведение компонент в больших системах. JML основывается на традиционной логике, но предложенный в диссертации язык спецификаций использует расширенную логику.Заметим, что для предложенного языка алгоритмически разрешима проблема проверки тождественной истинности формул для этого языка.

Основные результаты:

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

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

3.Основываясь на расширенных формулах,пред ставлена в качестве иллюстрации практической полезности разработанных инструментов экспертная система, предназначенная для того, чтобы давать советы студентам на разных этапах обучения в университете Хельван (Каир, Египет).

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

Практическая и теоретическая ценность.С теоретической точки зрения, представлено расширение логики высказываний и логики предикатов [11,33,44].Представлено расширение логики предикатов в виде языка описания свойств и отношений между объектами над конечными областями определения, достаточными для математического описания целочисленных программ, написанных на Паскале.

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

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

В диссертации разработана и реализована экспертная система для образовательного процесса в университете Хельван (Каир, Египет).Эта система выдаёт рекомендации и советы по выбору специальности на разных этапах обучения (бакалавриат, магистратура, аспирантура, получение звания доцента). Она реализована на языке программирования Пролог.

Разработан новый язык спецификаций, основывающийся на расширенной логике первого порядка.Этот язык может быть использован для записи доказательств правильности многих программ, реализованных на языке Паскаль и представленных в [17].Примеры спецификации ряда таких программ разработаны в диссертации.

Публикации.Основные результаты этой диссертации были опубликованы в изданиях на трех конференций в США, РФ и Швейцарии. Содержание работы.Краткий план содержания этой диссертации таков:

Во введении обосновывается актуальность темы исследования, формулируются цели задачи работы.Рассказаны исторические истоки, относящиеся к этой работе. Представлено краткое описание структуры диссертации.

В первой главе собраны необходимые все предварительные определения из [8] .Раздел 1 первой главы посвящен метаязыку (формализованное описание синтаксических понятий).

Раздел 2 посвящён определению пропозициональной формулы. В третьем разделе даны определения терма и предикатной формулы.

Четвёртый раздел посвящен изложению секвенциального исчисления предикатов.

Основной задачей второй главы является описание расширенного секвенциального исчисления высказываний при помощи линейных комбинаций расширенных пропозициональных формул.Это приводит к существенному сокращению длины и увеличению наглядности (читаемости) описаний расширенными пропозициональными формулами [26].

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

Третий раздел посвящён аксиомам и правилам вывода предложенного секвенциального исчисления. Раздел содержит определение секвенции, как слова, которое начинается со знака и состоит из списка формул (членов последовательности). В четвертом разделе доказаны теоремы, относящиеся к предложенному исчислению.Теорема 1 утверждает,что аксиомы и правила нашего секвенциального исчисления корректны в привычном арифметическом понимании знаков +,-■<,< .В теореме 2 доказана допустимость обратных правил для предложенного секвенциального исчисления. Теорема 3 доказывает полноту предложенного исчисления. Доказана . NP-полнота задачи выполнимости расширенной пропозициональной формулы.

В третьей главе основная задача заключается в том, чтобы представить расширенное исчисление предикатов первого порядка [6,27].В первом разделе даются определения атомарной формулы, линейной комбинации строк и другие.Также даётся определение расширенной предикатной формулы. Во втором разделе предъявлено секвенциальное исчисление предложенных расширенных предикатных формул [27].Сформулирована теорема 1, в которой доказано, что предложенное секвенциальное исчисление является консервативным расширением традиционной логики первого порядка. В третьем разделе представлены допустимость правила сечения и в четвертом разделе сформулирована теорема об эквивалентной замене.Теорема 4 о семантическом обосновании предложенных исчислений и лемма 1 о семантическом обосновании аксиом и правил исчисления.

В четвёртой главе описана экспертная система, которая позволяет обеспечить процесс обучения в университете Хельван (Каир, Египет). Она дает советы и предлагает студентам выбор специализации на разных этапах учёбы (бакалавриат, магистратура, аспирантура, подготовка к получению звания доцента).Вся база данных в этой части взята из информации по факультету естественных наук университета Хельван (Каир, Египет). Во введении к этой главе объясняется необходимость этой системы.Второй раздел этой главы относится к степени бакалавра, третий - магистра, четвертый — кандидата наук, и, наконец, последний — доцента.В каждом разделе представлены основные курсы с соответствующими градациями отметок и перечислены разные случаи в различных ситуациях, затем сформулированы правила, основываясь на которых, даны рекомендации. В конце каждого раздела приведены примеры целей для каждой программы системы использующих,соответствующие базы данных.Все эти подсистемы реализованы на языке Пролог.(См.например [30,34,36]).

Пятая глава посвящена предлагаемому языку спецификаций для записи утверждения о частичной корректности программ в целом [4] .В первом разделе представлены некоторые базовые концепции и определения языка спецификаций с кратким обзором JML—выражений.

Далее в этом разделе дано определение расширенного понятия терма в языке спецификаций.

Во втором разделе определена атомарная формула языка спецификаций. Также дано определение формулы языка спецификаций. Разделы 3 и 4 посвящены использованию языка спецификаций для утверждений о корректности программ, описанию аксиом и правил вывода из [24,45].В пятом разделе представлена основная задача этой главы: примеры записи утверждений о корректности программ на предложенном формальном языке спецификаций .Приведены примеры некоторых программ, реализованных на языке Паскаль из [17], с формализованными спецификациями, обеспечивающими корректность этих программ на предложенном языке спецификаций.

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

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

В приложении 1 и 2 излагаются дополнительные детали доказательства теоремы 2 из главы 2.

Заключение

Разработанный логический аппарат в главах 2 и з практическая применимость которого продемонстрирована в главах 4 и 5,обеспечивает возможность его более широкого полезного практического применения для описания решений задач искуственного интеллекта,особенно связанных нейросетями задачами классификациями линейными функциями.

1. Волгин Л.И., Левин В.И., Непрерывные логики, теория и применения, Таллин, 1991.

2. Карпенко А.С., Логики Лукасевича и простые числа, Наука, Москва, 2000,319 с.

3. Клини С.К., Введение в метаматематику, М.: Иностранная литература, 1957, 526 с.

4. Косовский Н.К., Элементы математической логики и ее приложения к теории субрекурсивных алгоритмов, Изд-во Ленинградского Университета, Ленинград, 1981.

5. Косовский Н.К., Уровневые логики, Записки научн. семинаров санкт—петербурского отдел. Математического института им.В.А.Стеклова, Издоние 200, 1995, с.72-82.

6. Косовский Н.К., Серия новых логических связок для проектирования электронных схем, Компьютерные инструменты в образовании, Изд—во центра профессионального обновленияинформатизация образования ", СПБ,N.2,2003, с.64—68.

7. Косовский Н.К., Дарвиш А.А., Расширение пропозиционального секвенциального исчисления списками и сложением, Современная логика, Теория задач, История и применение в науке, Материалы

8. VIII Российской международной научной конференциии, 24—26 июня, Санкт-Петербург, 2004, с.497-499.

9. Косовский Н.К., Тишков А.В., Логики конечнозначных предикатов на основе неравенств, Санкт-петербургского университета, Санкт Петербургб, 2000.

10. Тельпиз М.И., Представление булевых функций , Кибернетика, N.4, 1985, с.37—40.

11. Aho A.V., Ulman J.D., Foundations of computer science, Computer Science Press, New York, 1992.

12. Brachman R., Levesque H., Readings in knowledge representation, Morgan Kaufmann,los Altos, California, 1985.

13. Bratko I., Prolog programming for artificial intelligence, Addison Wesley, 2001.

14. Bundy A., Computer modeling of mathematical reasoning,Academic Press Professional,Inc., San Diego, 1985.

15. Buss S., Clote P., Cutting planes, connectivity and threshold logic, Archive for Mathematical Logic, 35,1996, pp.33 — 62.

16. Dawe M.S., Dawe C.M.,Prolog for computer science, Springer Verlage, 1994.

17. Dijkstra E.W., Dahl O-J, and Hoare CAR, Structured programming, Academic Press, 1972.

18. Dromey R.G., How to solve it by computer, Prentice Hall International Series in Computer Science, London, 1982.

19. Flesca S., Greco S., Leone N. and Ianni G.,Logics in artificial intelligence, Proceeding of the 8th European Conference, September 23-26, Vol 2424,Springer Verlage, 2002, pp.529-532.

20. Gabbay, M.Cheney, J., A sequent calculus for nominal logic, IEEE Symposium on logic in computer science, 13-17 July,2004, France, pp.139-148.

21. Gallier J.H., Logic for Computer science, foundations of automatic theorem proving,Harper& Row Publisher inc., New York, 1985.

22. Gary M.R., Johnson D.S.,Computers and intractability, series of books in mathematical science, W.H.Freeman and Company, New York, 1979.

23. Giorgio fumera, Fabio Roli, A theoretical and experimental analysis of linear combiners for multiple classifier systems, IEEE transactions on pattern analysis and machine intelligence,Vol.27, No.6, June, 2005, pp.942-956.

24. Goodman I.R., Gupta M.M., Nguyen H.T., and Rogers G.S.,Conditional logic in expert systems, Elsevier science publishers B.V., 1991.

25. Hoare C.A., An axiomatic basis of computer programming, Communications of the ACM, Vol.12, N.10,1969, pp.567-580.

26. Ince D.C., An introduction to discrete mathematics, formal system specification, and Z, Oxford University Press, New York, 1988.

27. Kossovski N.K., Darwish A.A., Prepositional sequent calculus with list construction and addition, The 8th World Multi-Conference on Systemic, Cybernetics and Informatics, July 18—21, Vol.1, Orlando, Florida, USA, 2004, pp.17-19.

28. Kossovski N.K., Darwish A.A., Two sequent calculuses with inequalities of linear combination, The 1st World Congress and School on Universal Logic, March 26th—April 3th, Montreux, Switzerland, 2005, pp.61-64.

29. Kossovski N.K., Tishkov A.V., Logical theory of Post logic with linear Order: Technical Report TR—97 — 11. Department of Informatics, University Paris-12, Paris, 1997, 9p.

30. Leavens Gary Т., Baker Albert L., and Ruby Clyde, Preliminary design of JML: A behavioral interface specification language for Java, Departmentof Computer Science, Iowa State University, December, 2004.

31. Levine R.I.,Diance E., and Edelson В.,A comprehensive guide to AI and expert systems: turbo pascal edition, McGraw Hill Book Company, 1988.

32. Lloyd J.W., Foundations of logic programming, Springer Verlage, 1987.

33. Luger G.F., Artificial intelligence, structures and strategies for complex problem solving, Addision Wesley, 2002.

34. Mandrioli D., Ghezzi C., Theoretical foundations of computer science, John Wiley& sons, 1987.

35. Marcellus D.H., Expert systems programming in turbo prolog, Prentice Hall, New Jersey, 1989.

36. McDermott, D., Doyle, J., Nonmonotonic logic 1. In: Artificial Intelligence, No. 13, 1980, pp.41 -72.

37. Merritt D., Building expert systems in prolog, Springer Verlag, New York, 1989.

38. Munakata Т., Foundations of the new artificial intelligence, Springer Verlag, New York, 1998.

39. Nerode A., Shore R.A., Logic for applications, Springer Verlage, New York, 1997.

40. Nilson N.J., Artificial intelligence, Morgan Kaufmann Publisher, 1998.

41. Nilsson U., Jan Maluszynski., Logic programming and prolog, John Wiley& Sons, 1990.

42. Raeth P.G., Expert systems, A software methodology for modern applications, IEEE Computer Society Press Reprint Collection, IEEE, 1990.

43. Roger Hult, Grey—Level morphology combined with an artificial neural networks aproach for multimodal segmentation of thehippocampus, The 12th International Conference on Image Analysis and Processing (ICIAP'03), IEEE, 2003, pp. 277-282.

44. Scheurer Т., Foundations of computing system development with set theory and logic, Addison Wesley, Cambridge, 1994.

45. Slonneger K., Kurtz В L., Formal syntax and semantics of programming languages, Addison Wesley, 1995.

46. Yang Shuyuan, Wang Min and Jiao Licheng, A new adaptive ridgelet neural network, Advances in neural networks ISNN, Second International Symposium on Neural Networks, May 30—June 1, Chongqing, China, 2005, pp.385-390.