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

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВ^№Ь*Й УНИВЕРСИТЕТ

л л

003055625

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

Герасимов Александр Сергеевич

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

05 13 11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

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

003055626

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

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

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

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

Оревков Владимир Павлович

кандидат физико-математических наук Тишков Артем Валерьевич

Ведущая организация

Санкт-Петербургский государственный политехнический университет

Защита диссертации состоится « » АС1-Р2 А Ц 2007 года в Ф ьо на заседании диссертационного совета Д 212 232 51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу 198504, Санкт-Петербург, Старый Петергоф, Университетский пр , д 28, математико-механический факультет Санкт-Петербургского государственного университета

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

Автореферат разослан « Л» МАРТА . 2007 года

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

диссертационного совета

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

I Мартыненко Б К

Общая характеристика работы

Актуальность темы. Интерес к многозначным (в частности, беско-нечнозначным) логикам объясняется их разнообразными применениями, включающими представление нечетких знаний и приблизительные рассуждения (см , например, [12, 14])

Многозначная логика как область математической логики развивалась параллельно с нечеткой логикой, восходящей к Заде [18, 3] Нечеткая логика Заде основана на теории нечетких множеств — множеств с размытыми границами, такое множество задается с помощью функции принадлежности, сопоставляющей элементу действительное число из отрезка [0,1] Нечеткой логикой в широком смысле (далее для краткости — нечеткой логикой) сейчас называют (см [15]) дисциплину, использующую понятия теории нечетких множеств для разработки методов прикладных приблизительных рассуждений Нечеткая логика используется в промышленных системах нечеткого контроля, например, в бытовых приборах Однако с формально-логической точки зрения методы нечеткой логики не представляются корректно обоснованными [14]

В последнее десятилетие активно идег процесс формализации нечеткой логики (см основополагающие труды [14, 12, 7]) В связи с этим математической нечеткой логикой (или нечеткой логикой в узком смысле) называют дисциплину, которая разрабатывает дедуктивные системы для нечеткой логики, рассматривая ее как многозначную логику, в стиле и со строгостью математической логики Бесконечнозиачная предикатная логика Лукасевича (ее описание может быть найдено, например, в [14]) является одной из основных многозначных логик, используемых для формализации нечеткой логики

Процесс становления математической нечеткой логики еще далек от завершения в связи с том, что нечеткая логика включает концепции, которые отсутствуют в многозначной лотке В частости, в нечеткой логике имеются лингвистические модификаторы «очень», «чрезвычайно», «вполне» и др Заде [3] применяет возведение функции принадлежности в квадрат для представления модификатора «очень», что делает формализацию нечеткой логики трудной Потому альтернативная и более простая формализация существенной черты нечеткой логики — модификаторов типа «очень» — является важным шагом в сближении математической нечеткой логики с нечеткой логикой в широком смысле, к тому же это расширяет область возможных применений математической нечеткой логики

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

товского типа (их можно найти, например, в [14, 12]), не подходящие для автоматического поиска доказательств

Для бесконечнозначной пропозициональной логики Лукасевича извес т-ны разнообразные методы поиска доказательств, в том числе разработанные в течение последних нескольких лег, например методы семантических таблиц [13, 17], секвенциальные исчисления [5, 10, 16] Особо отметим секвенциальное исчисление для уровневой логики [5] Логические связки уровневой логики позволяют записывать формулы логики Лукасевича Для распознавания аксиом секвенциального исчисления уровневой логики применяются методы линейного программирования, и этот подход развивается в данной работе

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Апробация работы. Результаты работы были представлены на VIII и IX Общероссийских научных конференциях «Современная логика проблемы теории, истории и применения в науке» (Санкт-Петербург 2004 и 2006 годы), Межвузовском конкурсе-конференции студентов, аспирантов и молодых ученых Северо-Запада «Технологии Microsoft в теории и практике

программирования» (Санкт-Петербург, 2005 год), Международной конференции «Устойчивость и процессы управления» (Санкт-Петербург, 2005 год), семинаре Санкт-Петербургского отделения Российской ассоциации искусственного интеллекта (Санкт Петербург, 2006 год), XVI Международной школе-семинаре «Синтез и сложность управляющих систем» (Санкт-Петербург, 2006 год), Десятой национальной конференции по искусственному интеллекту с международным участием КИИ-06 (Обнинск, 2006 год)

Публикации. Основные результаты опубликованы в работах [1' - 6']

Структура и объем диссертации. Диссертация состоит из 6 глав, списка литературы и 2 приложений Диссертация изложена на 194 страницах машинописного текста Основной текст диссертации занимает 168 страниц, приложения занимают 26 страниц Список литературы содержит 82 наименования

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

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

Вторая глава посвящена описанию предлагаемой логики (обозначаемой Ьд), секвенциального исчисления ЬдБ для нее и свойств этого исчисления [2', 1']

В первом разделе этой главы определяется язык логики Ьд и его семантика Неотъемлемой частью каждого предикатного символа является так называемый его отрезок истинностных значений [а, 6], где а,Ь — рациональные числа, а < Ь Термом является предметная переменная и предметная константа Атомарной форлщлой является любое рациональное число, пропозициональная переменная и предикатный символ с заключенным в скобки списком термов Формулами логики Ьд являются атомарные формулы, а также (А&Я), (А V В), (А -< В), д А, \/хА, 3хА, где А и В -формулы логики Ьд, д — рациональное число, х — предметная переменная Связки -< и д носят названия нечеткое неравенство и модератор соответствен] ю

Для задания семантики языка логики Ьд вводятся понятия интерпретации и оценки языка Эти понятия аналогичны традиционным, за исключением того, что здесь интерпретация сопоставляет предикатному символу предикат, который действует в отрезок действительных чисел, являющийся отрезком истинностных значений этого преди-

катного символа (каждой пропозициональной переменной сопоставляется действительное число из такого отрезка) Если заданы интерпретация и оценка, то каждая формула Л получает истинностное значение [Л], являющееся действительным числом, согласно следующим правилам [(Л&В)] = тт([А], [В]), [(Л V В)\ = тах([Л], [В]), [(Л -< В)} = [В] - [Л], [<7 А] = д [Л], [УхЛ] = т^Л], [ЗхЛ] = ьирх[Л] Формула называется общезначимой, если истинностное значение этой формулы неотрицательно во всякой интерпретации при любой оценке

Отметим, что, во-первых, модераторы реализуют увеличение или уменьшение истинностных значений формул, поэтому с помощью модераторов можно формализовать различные модификаторы нечеткой логики типа «очень» Во-вторых, утверждение о том, что во всякой интерпретации при любой оценке формула Л принимает истинностные значения, не меньшие (соответственно, не большие) рационального числа г, эквивалентно тому, что формула (г -< Л) (соответственно, (Л -< г)) общезначима В-третьих, любую формулу бесконечнозначной предикатной логики Лука-севича можно представить в виде формулы логики Ьд так что во всякой интерпретации при любой оценке истинностные значения этих формул совпадают

Приводится следующий пример формализации приблизительных рассуждений с помощью логики Ьд Из посылок (1) есш предмет мал, то его трудно разглядеть, и (2) предмет 2 очень мал, следует, что (3) предмет г довольно трудно разглядеть Введем предикат Р1[0,1](ж), который сопоставляет предмету х действительное число из отрезка [0,1], характеризующее степень малости этого предмета, и предикат Р2[0,1](у), аналогичным образом выражающий степень трудности разпядывания предмета у Модификатор «очень» формализуем с помощью модератора 1/2 , «довольно» — с помощью модератора 2/3 Указанное приблизительное рассуждение запишем в виде формулы логики Ьд ((Ух(Р1[0,1](а:) Р2[0,1](х)) & 1/2 Р1[0,1](г)) -< 2/3 Р2[0,1](г)) Таким образом, для обоснования этого приблизительного рассуждения достаточно доказать соответствующую ему формулу

В конце первого раздела второй главы доказана теорема о том, что множество общезначимых формул логики Ьд неперечислимо

Во втором разделе второй главы сформулировано безантецедентное секвенциальное исчисление ЬдБ для логики Ьд, и определены сопутствующие понятия Секвенцией называется конечный список формул логики Ьд (членов этой секвенции), разделенных запятыми, некоторые формулы могут повторяться, порядок формул в списке не имеет значения Секвенция называется общезначимой, если дизъюнкция всех ее членов общезначима (пустая секвенция в виде такой дизъюнкции представляется числом —1) Приводятся правила вывода, вводящие логические символы, кроме моде-

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

Далее определены аксиомы исчисления ЬдБ Каноническая цепь неравенств (КЦН) определяется следующим образом Формулы вида Р и д Р (где д — модератор, Р — атомарная формула) являются КЦН Если I и 3 - КЦН, то (.I ■< Л) является КЦН

Пусть дана секвенция й1 Удалим из 5 все члены, которые не являются КЦН, тогда полученная секвенция называется базовой подсеквенцией секвенции 5 Секвенция называется аксиомой, если базовая подсеквенция этой секвенции общезначима

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

В третьем разделе второй павы устанавливаются некоторые свойства исчисления ЬдБ Перечислим наиболее важные из них

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

2 Исчисление непротиворечиво

3 Безантецедентное секвенциальное исчисление для классической двузначной логики вкладывается в исчисление ЬдБ

4 Для логики Ьд не существует полное и семантически обоснованное исчисление

5 Исчисление ЬдБ неразрешимо

6 Исчисление ЬдБ полно для пропозиционального фрагмента логики Ьд

7 Пропозициональный фрагмент исчисления ЬдБ разрешим

8 Исчисление Ьдв допускает минус-нормализацию вывода

Поясним последнее свойство При так называемом поиске вывода заданной секвенции 5" сиизу вверх находят секвенции, из которых секвенция ¿> получается по одному из правил вывода, и для каждой наиденной секвенции, если она не является аксиомой, находят секвенции, из которых она получается по одному из правил вывода, и тд При этом по секвенции и правилу вывода требуется подбирать секвенции, которые являются посылками применения этого правила вывода, причем секвенция 5 должна быть заключением этого применения (т е требуется осуществлять контрприменение правила вывода) При контрприменении правил вывода исчисления ЬдБ, вводящих какой-либо выбранный логический символ, секвенции-посылки подбираются детерминированным образом, кроме того

стучая, когда осуществляется контрпримененне так называемого минус-правила Каждое из минус-правил исчисления ЬдБ (типа правила введения квантора существования в сукцедент секвенции в генценовском исчислении для клас сической двузначной лог ики) допускает бесконечный перебор термов для подстановки в посылку при контрприменении

Для классической двузначной логики первого порядка известны секвенциальные исчисления (см , например, [4], а также [6, 11]), в которых устранен бесконечный перебор термов дчя подстановки при контрприменениях минус-правил соответствующих секвенциальных исчислений Такое устранение бесконечного перебора термов названо минус-нормализацией [С] Однако упомянутые работы (и все известные нам другие работы) не содержат доказательств равнообъемностп предложенных секвенциальных исчислений и какого-либо из традиционных секвенциальных исчислений для классической двузначной логики

В настоящей работе формулируется ограничение на термы для подстановки (подставляемый терм — один из конечного числа термов, входящих в заключение минус-правила) и доказывается, что при этом не изменяется объем выводимых секвенций (Тогда обоснование минус-нормализации для исчисления классической двузначной логики следует из свойства 3 )

В последнем, четвертом разделе второй главы формулируется подлоги-ка Ьд2 логики Ьд и секвенциальное исчисление Ьд2Б для этой подлогики В формулах подлогики Ьд2 использование логической связки -< ограничено так, что распознавание аксиомы исчисления Ьд2Б сводится к проверке несовместности системы линейных неравенств, каждое из которых имеет не более двух членов Для решения таких задач существует сильно полиномиальный алгоритм (такой алгоритм описан в пятой главе данной работы), тогда как для распознавания аксиом исчисления ЬдБ известны только полиномиальные алгоритмы Подлогика Ьд2 оказывается достаточно выразительной для первоначального моделирования областей нечетких знаний В третьей главе описан алгоритм поиска вывода и доказаны его свойства

При поиске вывода заданной секвенции в исчислении ЬдБ снизу вверх естественным образом строится дерево поиска вывода, корнем которого является исходная секвенция, непосредственными потомками корня — секвенции, являющиеся посылками коптририменения некоторого правила вывода к корневой секвенции, и тд (считается, что это дерево растет от корня вверх) В тот момент, когда все секвенции-листья оказывают ся аксиомами, дерево поиска вывода становится деревом вывода, т е вывод найден Несмотря на го, что бесконечный перебор термов для подстановки при конгрприменепиях минус-правил может быть устранен, задача подбора термов, хотя и упростилась, все равно остается Воспользуемся так называемым методом метапеременных вместо подстановки конкретного тер-

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

Предлагаемый алгоритм Prove [3'] ищет вывод заданной секвенции, строя заготовку вывода При контрприменении минус-правила и введе нии метапеременной с ней ассоциируется подстановочное множество — конечное множество термов, содержащее все термы, только которые и достаточно подставлять вместо этой метапеременной в соответствии с ограничением минус-нормализации Тогда для того, чтобы подобрать значения для метапеременных, превращающие заготовку вывода в дерево вывода, производится унификация —- конечный перебор термов из подстановочных множеств метапеременных, входящих в заготовку вывода, и при этом переборе выбираются значения метапеременных, при которых заготовка превращается в дерево вывода

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

Во втором разделе описаны шаги главного алгоритма Prove и вспомогательных алгоритмов алгоритма, проверяющего, является ли секвенция аксиомой, и алгоритма, проводящего унификацию Также сформулированы требования к вспомогательному алгоритму, называемому тактикой по иска вывода такой алгоритм по заготовке вывода сообщает, когда нужно провести унификацию, и выбирает (а) секвенцию-лист S, (Ь) правило вывода (Я), контрприменение которого следует осуществить, и (с) вхождение логического символа в S, которое может быть введено в S применением правила (R) В конце второго раздела приводится пример поиска вывода, с комментариями

В третьем разделе доказаны свойства вспомогательных алгоритмов и главного алгоритма Prove Итогом является следующая теорема

Теорема Пусть алгоритм Prove использует любую тактику поиска вывода, S — секвенция, подаваемая на вход алгоритма Prove Тогда верны следующие утверждения

(1) Если алгоритм Prove выдал ответ «выводима», то секвенция S выводима в исчислении LqS

(2) Если алгоритм Prove выдал ответ «невыводима», то секвенция S невыводима в исчислении LqS

(3) Пусть секвенция S не содержит кванторов Тогда алгоритм Prove выдает ответ «выводима», если секвенция S выводима в исчисле-

кии LqS, и выдает ответ <гневыводимо,», если секвенция S иевыво-дима в исчислении LqS

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

В четвертой главе описана программная реализация алгоритма поиска вывода [3'] Этот алгоритм реализован на языке программирования Java в виде интерфейса прикладного программирования (ИПП), который предоставляет программный интерфейс для доступа к своим функциональным возможностям В начале этой главы кратко описывается назначение основных классов, сгруппированных в пакеты, и приводятся диаграммы классов, изображающие иерархии логических символов, термов и формул Затем определяется политика разделения объектов в программном представлении формул (с помощью синтаксических деревьев с возможно раздетяемыми листьями) и секвенций Эта политика, с одной стороны, позволяет однозначно и эффективно идентифицировать вхождение неатомарной подформулы в формулу, а, с другой стороны, позволяет существенно экономить память при поиске вывода, допуская общие формулы в разных секвенциях

Далее описываются основные компоненты реализации алгоритма поиска вывода Отметим следующие ключевые особенности

В этом ИПП тактика поиска вывода задается с помощью интерфейса Tactics Главный алгоритм поиска вывода может использовать любую тактику, являющуюся реализацией этого интерфейса (Такая архитектура соответствует образцу проектирования стратегия [8] )

Каждое правило вывода представлено объектом, который имеет метод, осуществляющий контрприменение этого правила Главный алгоритм поиска вывода делегирует контр применение правила вывода, выбранного тактикой, самому этому правилу Таким образом, правила вывода могут быть легко изменены

Каждая система линейных неравенств, получаемая при распознавании аксиом, проверяется на несовместность вспомогательным алгоритмом, описанным в пятой гпаве данной работы, если все неравенства системы двучленные, иначе — функцией Findlnstance системы компьютерной алгебры Mathematica (посредством J/Lmk — инструментария, связывающего программу на Java с Mathematica)

В конце четвертой главы приведен систематический обзор предоставляемого программного интерфейса для поиска вывода

Объем написанного программно! о кода, включая реализацию алгоритма решения систем линейных двучленных неравенств, составляет около 9000 строк

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

Алгоритм называется сильно полиномиальным (см , например, [9]), если (а) он полиномиален по числу шагов при реализации на машине Тьюринга, и (Ь) число элементарных арифметических операций (сложение, вычитание, умножение, деление, сравнение), выполняемых им над рациональными числами, ограничено полиномом от числа целых чисел на входе

Упомянутые алгоритмы были предложены в [2], там же установлено условие (Ь) определения сильно полиномиального алгоритма

В настоящей диссертационной работе осуществлена детализация этик; алгоритмов, причем добавлены необходимые шаги (без которых описания алгоритмов из [2] были некорректны), и разработан вспомогательный алгоритм удаления избыточных неравенств (см [5', 6']) Доказана корректность описанных в настоящей диссертации алгоритмов, т е алгоритм проверки совместности систем выдает ответ «совместна», если входная система совместна, и выдает ответ «несовместна», если входная система несовместна (аналогичное утверждение установлено и для алгоритма решения систем) Далее определена вычислительная модель, близкая к равнодоступной адресной машине с логарифмическим весовым критерием (см [1]), и получена полиномиальная оценка временной сложности описанных алгоритмов [6'] Установлена полиномиалыюсть числа шагов этих алгоритмов при реализации на машине Тьюринга, что позволяет также доказать их сильную полиномиальность

В последнем разделе пятой главы описана реализация алгоритма на языке Java в виде интерфейса прикладного программирования [4'] В этой реализации участвуют 2 алгоритма с похожими шагами упомянутый алгоритм решения систем с удалением избыточных неравенств и алгоритм, основанный на обычном методе исключений переменных Одна из основных задач объектно-ориентированного программирования — вычленение общего поведения с целью повторного использования кода — решена с помощью шаблонного метода [8]

Наконец, приводятся результаты экспериментов по сравнению производительности реализованного автором диссертации алгоритма решения систем и алгоритма, представленного функцией Findlnstance системы ком-

пьютерной алгебры Mathematica Эксперименты проводились на одном и гом же персональном компьютере На решение систем из нескольких тысяч неравенств реализованный алгоршм затрачивает несколько секунд, а Mathematica — несколько десятков минут На решение систем из нескольких десятков тысяч неравенств реализованный алгоритм затрачивает до нескольких десятков секунд, a Mathematica не заканчивает работу за 12 часов Эти результаты говорят о том, что для решения систем линейных двучленных неравенств реализованный алюритм намного эффективнее алгоритма, используемого в системе компьютерной алгебры Mathematica

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

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

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

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

[1] А то А , Хопкрарт Дж , Улълшн Дж Построение и анализ вычислительных алгоритмов / Пер с англ — М Мир, 1979

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

[3] Заде JI Понятие лингвистической переменной и его применение к принятию приближенных решении / Пер с англ — М Мир, 1976

[4] Катер С Упрощенный метод доказатетьства для элементарной логики // Математическая теория логического вывода / Под ред А В Идельсона, Г Е Минца - М Наука, 1967 - С 200-207

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

[6] Маслов С Ю , Минц Г Е Теория поиска вывода и обратный метод / / Чень Ч , Ли Р Математическая логика и автоматическое доказательство теорем — М Наука, 1983 - С 291-314

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

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

[9] Chandru V, Rao М R Linear programming // Algorithms and theory of computation handbook / Ed by M J Atallah — CRC Press, 1999

[10] Ciabattom A , Fermuller С G, Metcalfe G Uniform rules and dialogue games for fuzzy logics // LPAR / Ed by F Baader, A Voronkov — Vol 3452 of Lecture Notes in Computer Science — Spnnger, 2004 — Pp 496-510

[11] Degtyarev A , Voronkov A Equality reasoning m sequent-based calculi // Handbook of Automated Reasoning / Ed by A Robinson, A Voronkov — Elsevier, 2001 - Vol 1 - Pp 611-706

[12] Gottwald S A Treatise on Many-Valued Logics — Baldock Research Studies Press, 2001

[13] Hahnle R Many-valued logic and mixed integer programming //Annals of Mathematics and Artificial Intelligence — 1994 — Vol 12, no 3-4 — Pp 231-263

[14] Hajek P Metamathematics of Fuzzy Logic — Dordrecht Kluwer Academic Publishers, 1998

[15] Hdjek P What is mathematical fuzzy logic // Fuzzy Sets and Systems — 2006 - Vol 157, no 5 - Pp 597-603

[16] Metcalfe G , Olivetti N , Gabbay D M Lukasiewicz logic from proof sys tems to logic programming // Logic Journal of the IGPL — 2005 — Vol 13, no 5 - Pp 561-585

[17] Olivetti N Tableaux for Lukasiewicz infinite-valued logic // Studia Logica - 2003 - Vol 73, no 1 - Pp 81-111

[18] Zadeh L A Fuzzy logic and appioximate reasoning // Synthese — 1975 - Vol 30 - Pp 407-428

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

[1'[ Герасимов А С Бесконечпозначная предикатная логика со связкой для усиления утверждений // Современная логика проблемы теории, истории и применения в науке Материалы IX Общероссийской научной конференции (Санкт-Петербург, 2006) - СПб 2006 - С 348-350

[2'] Герасимов А С Предикатная логика на основе секвенциального исчисления, предназначенная для моделирования непрерывных шкал // Десятая национальная конференция по искусственному интеллекту с международным участием КИИ-06 (Обнинск, 2006) Труды конференции — М Физмаглит, 2006 - С 339-347

[3'[ Герасимов А С Программная реализация поиска доказательств в бес-конечнозначной предикатной логике, основанной на линейных неравенствах // Материалы XVI Международной школы-семинара «Синтез и сложность управляющих систем» (Санкт-Петербург, 2006) / Под ред О Б Лупанова — М Изд-во механико-математического факультета МГУ, 2006 - С 30-35

[4'] Герасимов А С Разработка ИПП для решения задачи определения совместности систем линейных двучленных неравенств // Технологии Microsoft в теории и практике программирования Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада — СПб Изд-во Политехи ун-та, 2005 — С 161-162

[5'] Герасимов А С, Косовский Н К Истинно полиномиальный алгоритм определения совместности систем линейных двучленных неравенств // Устойчивость и процессы управления Труды международной конференции (Санкт-Петербург, 2005) / Под ред Д А Овсянникова, Л А Петросяна - СПб СПбГУ, НИИ ВМ и ПУ, ООО ВММ, 2005 -С 779-785

[6'[ Герасимов А С, Косовский Н К Оценка сложности истинно полиномиального алгоритма проверки совместности систем линейных двучленных неравенств // Вестник С-Петербург ун-та Сер 10 — 2006 - № 2 - С 16-21

Подписано в печать 06 03 2007 Формат бумаги 60 х 84 1/16 Бумага офсетная Печать ризографическая Уел печ л 1,0 Тираж 100 экз Заказ 3942

Отпечатано в отделе оперативной полиграфии НИИХ СПбГУ 198504, Санкт-Петербург, Старый Петергоф, Университетский пр 26

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

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

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

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

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

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

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

Заключение

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