WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 || 3 |

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

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

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

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

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

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

5. Исчисление LqS неразрешимо.

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

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

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

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

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

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

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

В третьей главе описан алгоритм поиска вывода и доказаны его свойства.

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

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

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

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

Во втором разделе описаны шаги главного алгоритма P rove и вспомогательных алгоритмов: алгоритма, проверяющего, является ли секвенция аксиомой, и алгоритма, проводящего унификацию. Также сформулированы требования к вспомогательному алгоритму, называемому тактикой поиска вывода: такой алгоритм по заготовке вывода сообщает, когда нужно провести унификацию, и выбирает (a) секвенцию-лист S, (b) правило вывода (R), контрприменение которого следует осуществить, и (c) вхождение логического символа в S, которое может быть введено в S применением правила (R). В конце второго раздела приводится пример поиска вывода с комментариями.

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

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

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

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

(3) Пусть секвенция S не содержит кванторов. Тогда алгоритм P rove выдает ответ выводима, если секвенция S выводима в исчислении LqS, и выдает ответ невыводима, если секвенция S невыводима в исчислении LqS.

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

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

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

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

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

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

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

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

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

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

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

В настоящей диссертационной работе осуществлена детализация этих алгоритмов, причем добавлены необходимые шаги (без которых описания алгоритмов из [2] были некорректны), и разработан вспомогательный алгоритм удаления избыточных неравенств (см. [5, 6 ]). Доказана корректность описанных в настоящей диссертации алгоритмов, т.е. алгоритм проверки совместности систем выдает ответ совместна, если входная система совместна, и выдает ответ несовместна, если входная система несовместна (аналогичное утверждение установлено и для алгоритма решения систем).

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

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

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

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

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

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

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

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

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

[4] Кангер С. Упрощенный метод доказательства для элементарной логики. // Математическая теория логического вывода. / Под ред.

А. В. Идельсона, Г. Е. Минца. М.: Наука, 1967. С. 200–207.

[5] Косовский Н. К. Уровневые логики. // Записки научных семинаров Петербургского отделения Математического института РАН.

Т. 220. СПб: Наука, 1995. С. 72–82.

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

Pages:     | 1 || 3 |






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»