Расширение предикатных формул линейными неравенствами и списками для спецификации программ тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Ашраф Абд Эль-Фаттах Мустафа Дарвиш

• Ашраф Абд Эль-Фаттах Мустафа Дарвиш
• кандидат физико-математических наук
• 2006

Оглавление диссертации кандидат физико-математических наук Ашраф Абд Эль-Фаттах Мустафа Дарвиш

ВВЕДЕНИЕ

ОГЛАВЛЕНИЕ

Глава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,обеспечивает возможность его более широкого полезного практического применения для описания решений задач искуственного интеллекта,особенно связанных нейросетями задачами классификациями линейными функциями.

Список литературы диссертационного исследования кандидат физико-математических наук Ашраф Абд Эль-Фаттах Мустафа Дарвиш, 2006 год

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.