Разработка и реализация алгоритма поиска вывода в расширении бесконечнозначной предикатной логики Лукасевича тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Герасимов, Александр Сергеевич

• Герасимов, Александр Сергеевич
• кандидат физико-математических наук
• 2007

Оглавление диссертации кандидат физико-математических наук Герасимов, Александр Сергеевич

1. Введение и предварительные сведения

1.1. Актуальноегь решаемых задач и обзор близких работ

1.1.1. Бесконечнозначная предикатная логика Лукаеевича

1.1.2. Усиление выразительности логики Лукаеевича

1.1.3. Разработка методов и средств для автоматического доказательства в логике Лукаеевича.

1.1.4. Реализация эффективного алгоритма решения систем линейных двучленных неравенств.

1.2. Цели рабош

1.3. Краткое содержание работы.

2. Расширение бесконечнозначной предикатной логики Лукаеевича

2.1. Язык логики и его семантика.

2.1.1. Язык логики.

2.1.2. Семантика.

2.1.3. Соотношение с логикой Лукаеевича.

2.2. Секвенциальное исчисление.

2.2.1. Правила вывода

2.2.2. Аксиомы.

2.3. Некоюрые свойства исчисления.

2.3.1. Семантическое обоснование исчисления.

2.3.2. Непротиворечивость исчисления.

2.3.3. Связь с исчислением для классической двузначной логики

2.3.4. Вопросы полноты и разрешимости исчисления

2.3.5. Минус-нормализация вывода.

2.4. Подлогика двучленных нечетких неравенств. G

3. Алгоритм поиска вывода

3.1. Идея алгоритма и основные определения.

3.2. Описание шагов алгоритма.

3.2.1. Алгоритм Is Axiom.

3.2.2. Алгоритм Unify.

3.2.3. Требования к алгоритму Tactics.

3.2.4. Главный алгоритм Prove.

3.2.5. Пример поиска вывода.

3.3. О корректности алгоритма.

3.3.1. Свойства алгоритма Is Axiom.

3.3.2. Свойства алгоритма Unify.

3.3.3. Свойства главного алгоритма Prove.

3.3.4. Выбор алгоритма Tactics.

4. Программная реализация алгоритма поиска вывода

4.1. Общая структура.

4.1.1. Пакет prover.

4.1.2. Пакет prover.calculus.

4.1.3. Пакет prover. calculus .rules.

4.1.4. Пакет prover.calculus.syntax.

4.2. Представление формул и секвенций.

4.3. Сишаксический анализатор.

4.4. Детлизация алгоритма поиска вывода.

4.4.1. Заготовка вывода.

4.4.2. Тактики поиска вывода.

4.4.3. Контрприменение правила вывода.

4.4.4. Унификация и распознавание аксиом.

4.5. Предоставляемый программный интерфейс.

4.5.1. Создание формул и секвенций

4.5.2. Поиск вывода секвенции.

4.5.3. Получение информации о ходе поиска вывода

5. Алгоритм решения систем линейных двучленных неравенств и его программная реализация

5.1. Алгоритм проверки cobmccthocih систем.

5.1.1. Постновка задачи и основные определения.

5.1.2. Метод исключений переменных.

5.1.3. Алгоритм добавления ограничения в систему.

5.1.4. Главный алгоритм проверки совместности систем

5.2. Оценка временной сложности алгоритма проверки совместности систем

5.2.1. Вычисли юльная модель.

5.2.2. Представление системы в памяти.

5.2.3. Оценка временной сложности.

5.3. Алгоритм решения сисхем.

5.4. Программная реализация алгоритма решения сисхем

5.4.1. Общая сфуктура.

5.4.2 Декомпозиция алгоритмов.

5.4.3. Предоставляемый программный интерфейс.

5.4.4. Экспериментальные результаты

Введение диссертации (часть автореферата) на тему «Разработка и реализация алгоритма поиска вывода в расширении бесконечнозначной предикатной логики Лукасевича»

предварительные сведенияВ этой вводной главе приводится аннотация данной диссертационнойработы, синтаксис и семантика бесконечнозначной предикатной логикиЛукасевича, обзор работ, близких к этой диссертации по теме исследова-ния, и обоснование актуальности направлений исследований, разрабаты-ваемых в данной диссертации. Затем ставятся цели этой дассертациии излагается краткое содержание следуппцит глав.Краткая характеристика работы. В данной работе нродлагае1ся логика более выразительная, чем бесконочнозначная предикатная логика Лу-касевича. Язык нредложенной логики расншряст язык логики Лукасевича'шк, что в предложенной логике выразимы различные модификаторы тина«очень», близкие к введенным Заде. Для нредложенной логики сформу-лировано секвенциальное исчисление, аксиомы коюрого раснознаются сномон1,ыо меюдов линейного программировании. Установлен ряд свойствэтого исчисления, ориентированных на автоматизацию ноиска логическоговывода. Рсиработан алгоритм поиска вывода в предложепном исчислении.Доказаны свойства этого а;н'оритма, отражающие различные аспекты егокорректности. А;пюритм ноиска вывода реализован в виде ин'1ерфейса при-кладного нрограммирования на языке нрограммиронания Java. Доработанби реализован ajH'opHi'M проверки совместности (и нахождения решения) си-стем линейных двучленных неравенств, коюрый используется в качествевс11омога'1ельного алюритма для эффективного распознавания некоторыхаксиом предложенного исчисления. Получена оценка временной сложностиэтого ajH'opHTMa в формальной вычислительной модели.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Герасимов, Александр Сергеевич

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

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

1. Сформулировано секвенциальное исчисление для бесконечнозначной предикатной логики Лукасевича, расширенной модификаторами типа «очень», коюрые восходят к нечеткой логике Заде.

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

3. Разработан алгоритм поиска вывода в предложенном секвенциальном исчислении. Доказаны свойства разработанного алгоритма, отражающие различные аспекты его корректности.

4. Алгоритм поиска вывода реализован в виде интерфейса прикладного программирования.

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

0. Алгоритм решения систем линейных двучленных неравенств реализован в виде ишерфейса прикладного программирования.

Научная новизна результатов

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

Теоретическая и практическая ценность результатов

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

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

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

Заключение

Список литературы диссертационного исследования кандидат физико-математических наук Герасимов, Александр Сергеевич, 2007 год

1. Алгорифм машинного поиска сстсствеипого логического вывода в ис-числении иысказынаний, / Н. А. Шанин, Г, В. Давыдов, Ю. Маслови др. - М., Л.: Наука, 1965.

2. Лрнолд .К, Гослинг До1С., Холмс Д. Язык программирования Java. / Пер. с англ.— М.. Издательский дом «Вильяме», 2001.

3. Ахо А., Сети Р., Ульман Дою. Комнилятор1л: нринципы, технологии и инструменты. / Пер. с англ.— М.: Изда'1ел1)Ский дом <'<Вильямс»,2001.

4. Ахо А., Хопкрофт Дж., Ульман Дою. Пост[)ооние и анализ вычисли- тельных гипюритмов. / Пер. с англ. — М.: Мир, 1979.

5. Аго А., Хопкрофт Дою., Ульман Дою. Структуры данных и aJнюpиг- мы. / Пер. с англ.— М.: Издательский дом «Вильяме», 2000.G. Бадд Т. Обьек'пю-ориентированпое программирование в действии. /Пер. с англ. — СПб: Питер, 1997.

6. Биркгоф Г. Теория репюток. / Пер. с англ. — М.: Паука, 1984.

7. Буч Г. Обьектно-ориентированный анализ и проектирование с приме- рами приложений на C f + . / Пер с англ.— Второе изд.— М.: Изда-Бином, 1998.

8. Буч Г., Рамбо Дою., Доюекобсон А. Язык UML. Руководство нользо- вателя. / Пер. с англ. — М.: ДМК П1)есс, 2004.160

9. Герасимов А. С, Косовский Н. К. Оценка сложности истинно нолино- миального алгоритма нроие|)ки совмосгности систем линейных дву-чле1Н1ых неравенств. // Вестник -Петербург, ун-та. Сер. 10.—200G. - Л^^ 2. - 16-21.

10. Гэри М., До1сонсон Д. Вычислительные маншны и труднорешаемые задачи. / Пер. с англ. — М.: Мир, 1982.

11. Давыдок Д. В О совместности сис'1ем двучленных линейных нера- венств. // Косовский Н. К., Тишков А. В. Логики конечнозначных нре-дикатов на основе неравенств.— СПб: Изда'1ельство -Петерб. уни-верситета, 2000. - 246-268.

12. Заде Л. Понятие лингвистической неременной и ею нрименение к нри- нятию нриближенных ренюний. / Пер. с англ. — М • Мир, 1976.

13. Зиглер К. Меюды нроектирования нрограммных сис1ем. / Пер. с англ. - М.: Мир, 1985.

14. Кангер Унрощенный меюд доказательства для элементарной ло- гики. // Математическая теория логического вьнюда. / Под ред.А. В. Идельсона, Г. Е. Минца. - М.: Паука, 1967. - 200-207.

15. Клини К. Введение в метаматематику. / Пер. с англ.— М.: Изда- тельство иностранной личературы, 1957.

16. Клини К. Математическая логика. / Пер. с англ. — М.: Мир, 1973. 24[ Колмогоров А. Н., Драгалин А. Г. Математическая логика. — М.: Еди-'юриал УРСС, 2004.

17. Комендантский В. Е. Меюд резолюций в сметанной логике Поста. // Труды семинара логического цен1ра ИФ РАП, вын. XVI.— 2002.—С. 64-74.

18. Кормен Т., Лейзерсон Ч., Ривест Р. Алгоритмы: ностроение и анализ. / Пер. с англ. - М.: МЦПМО, 1999.162

19. Косовский Н. К. Уропновыо логики. // Записки научных сомина- ров По гербу ргского отделения Математического института РАН.—Т. 220. - СПб: Наука, 1995. - 72-82.

20. Лисков В., Гатзг Дою. Использование абсхракций и снецификаций при разработке про1'рамм. / Hep. с англ.— М.: Мир, 1989.

21. Матулис В. А. Два варианта классического исчисления нредикатов без структурных правил вывода. // Доклады Академии наук СССР. —1962.-Т. 147.-С. 1029-1031.163

22. Мендельсон Э. Виедение в ма'1ематич{Ч'ку1о логику. / Пер. с англ.— М.: Наука, 1984.

23. Ноаак В., Перфильева И., Мочкорж И. Математические ирипципы нечеткой логики. / Пер. с англ. — М.: Физматлит, 2006.

24. Одинцов И. О. Профессиональное нрограммирование. Сис1емный иод- ход - 2-е изд. - СПб: БХВ-Пегербург, 2004.

25. Оревков В. П. Обратный метод иоиска вывода. // Адаменко А. П., Кучуков А. М. Логическое нрограммирование и Visual Prolog. — СПб:БХВ-Пеiep6ypr, 2003. - 952-965.

26. Приемы объектно-ориентированного проектирования. Паттерны про- ектирования. / Пер. с англ. / Э. Гамма, Р. Хелм, Р. Джонсон,Дж. Влиссидес. - СПб: Питер, 2001.

27. Родлеере X. Теория рекурсивных функций и эф(1)ективная вычисли- мость. / Пер. с англ — М . Мир, 1972.

28. Смирнова Е. Разрабо1ка и реализация aJиюpитмa обработки нечет- ких данных в многоуровневых логиках: Диссертация на соиск. учен.cieH. канд. физ.-мат. наук. / Санкт-Пегербургский государс'1 венныйуниверситет. — Санкт-Петербург, 2002.

29. Соммервилл И. Ннженерия нрограммного обесиечения. / Пер. с англ. — 6-е изд. — М.: Издательский до.м <'<Вильямс>/, 2002.164

30. CJрейвер A. Тео1)ия линейного и целочисленного нрограммирования. / Пор. с англ. - М.: Мир, 1991.

31. Фаулер М., Скотт К. UML в кратком изложении. Применение стан- дартного языка объектного моделирования. / Пер. с англ. — М.: Мир,1999.

32. Хаптер Р. Проектирование и конструирование комниляторов. / Пер. с англ. — М.: Финансы и сштисгика, 1984.

33. Daaz M., FcrmuUer C. G., Salzer G. Automated deduction for many- valued logics. // Handbook of Automated Reaboning. / Ed. by A. Robin-son, A. Voronkov. - Elsevier, 2001. - Vol. 2. - Pp. 1355-1402.

34. Chandui V., Rao M. R. Linear piogiamming. // Algorithms and theoiy of computation handbook. / Ed. by M. J. Atallah. — CRC Piebs, 1999.

35. Ciabattoni A., Fermiiller С С, Metcalfe G. Unifoim rules and dialogue games for fuzzy logics. // LPAR / Ed. by F. Baader, A. Voronkov. —Vol. 3452 of Lecture Notes in Computer Science. — Springer, 2004. —Pp. 496-510.

36. Cohen E., Meguldo N. Improved algorithms for linear inequalities with two variables per inequality. // SI AM Journal on Computing.— 1994.—Vol. 23, no. 6. - Pp. 1313-1347.

37. Degtyaiev A., Vownkov A. EqwdWty reasoning in sequent-based calculi. // 165Handbook of Automated Reabonirig. / Ed. by A. Robinson, A. Voronkov. —Elsovier, 2001. - Vol. 1. - Pp. 611-706.

38. Hdjck P. Metamathematics of Fuzzy Logic. — Dordrecht: Kluwer Academic Publishers, 1998.

39. Hdjek P. What is mathematical fuzzy logic. // Fuzzy Sets and Systems. — 2006. - Vol 157, no. 5. - Pp. 597-603..62] Ua%j L. Axiomatization of the infinite-valued predicate calculus. // Journalof Symbolic Logic. - 1963. - Vol. 28, no. 1. - Pp. 77-86.

40. Hochbaum D. S., Naor ,/. Simple and fast algorithms for linear and in- teger programs with two variables per irrequality. // SI AM Journal onComputing. - 1994. - Vol. 23, no. 6. - Pp. 1179-1192.

41. Java 2 Platform Starrdard Edition 5.0. http://java.sun.com/j2se/1.5.0.

42. Java 2 Platform Standard Edition 5.0 API Specificatiorr. http://Java.sun.com/j2se/l.5.0/docs/api.166

43. Javadoc, an API documoiitatioii generator, h t t p : / / j ava.sun.com/j 2se/j avadoc.

44. J/Link, a toolkit that integrates Mathematica and Java, http://www.wolfram.com/solutlons/mathlink/jlink.

45. Karmarkar N. A new polynomial-time algorithm for linear program- ming. / / Comhinatonca. - 1984. - Vol. 4, no. 4. - Pp. 373-396.

47. Mathematica, a computer algebra system. http://www.wolfram.com/products/mathematica.

48. Megiddo N. Towards a genuinely polynomial algoiithm for linear pio- gramming. / / SIAM Journal on Computing. — 1983. — Vol. 12, no. 2. —Pp. 347-353.

49. Metcalfe G., Olivetti N., Gabbay D. M. Lukasiewicz logic: from proof sys- tems to logic piogiamming. / / Logic Journal of the IGPL— 2005.—Vol. 13, no. 5. - Pp. 561-585.

50. Metcalfe G., Olivetti N., Gabbay D. M. Secfuent and liypersecjuent calculi for abelian and Lukasiewicz logics. / / AGM Transactions on Gomputa-tional Logic. - 2005. - Vol. 6, no. 3. - Pp. 578-613.

51. Mundici D., Olivetti N. Resolution and model building in the infinite- valued calculus of Lukasiewicz. / / Theoretical Gomputer Science.—1998. - Vol. 200, no. 1-2. - Pp. 335-366.

52. Olivetti N. Tableaux for Lukasiewicz infinite-valued logic. / / Studia Logi- ca. - 2003. - Vol. 73, no. 1. - Pp. 81-111.167

53. Pavelka J. On fuzzy logic I, II, III, / / Zeitschnft fur Mathematische Loijik mid Gnmdlagcn der Mathematik. - 1979. -- Vol. 25. - Pp. 45-52,119-134,447-464.

54. Pnjatclj A. Bounded contraction and Gentzen-style formulation of 1.ukasiewicz logics. / / Studia Logica. — 1996. — Vol. 57. — Pp. 431-456.

55. Scarpellim B. Die Nichtaxiomatisierbarkeit des Unendlichwertigen Pradikatenkalkuls von Lukasiewicz. / / ^Journal of Symbolic Logic. —1962. - Vol. 27, no 2. - Pp. 159-170.

56. Wagner H. A new resolution calculus for the infinite-valued propositional logic of Lukasiewicz. / / Int. Workshop on Fiist-Oidei Theoieni Proving. /Ed. by R. Caferra, G. Salzer. - 1998. - Pp. 234-243.

57. Zadeh L. A. Fuzzy sets. / / Information and Control— 1965.— Vol. 8, no. 3. - Pp. 338-353.

58. Zadeh L. A. Fuzzy logic and approximate reasoning. / / Synthese.— 1975. - Vol. 30. - Pp. 407-428.168