Алгоритмы выводимости в рациональнозначных логиках для представления знаний

• Автор: Тишков, Артем Валерьевич
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Санкт-Петербург
• Количество страниц: 103 с.

ГЛАВА I. Шт . Специфические правила вывода исчщрениях 1К5 и УЪэ. Добавление сортов для конечных множеств. Выполнимость формул в теориях линейных неравенств. ГЛАВА 2. Предикатные формулы. Интерпретация формул . Вложение рассматриваемых логик в двузначную. Правила вывода для внутренних формул
ГЛАВА 3. Имеется трехместная функция дин залиси условных выражений. Последним в сигнатуре записан одноместный предикат неотрицательности аргумента. Целочисленная теория супординейных неравенств . Ах. Ах. Ь, Аа6. А.0 о, Аа1. I, ЦА. Ах. Ааб. Алб. Ь г i, Ая. Ат. Ааб. X 0 с i, . Ааб. Для всех указанных теорий строятся исчисления для чистых секвенций. Исчисления обладают свойством обратимости всех правил, которое облегчает поиск вывода. В этой же главе доказаны следующие теоремы о сложности вывода в втих исчислениях. Все теории, для которых существуют полиномиальные алгоритмы распознавания аксиом, разрешимы алгоритмом из класса ВТМЕ0. Для теорий и и можно воспользоваться, например, алгоритмом Хчияна, для теорий ЗЪг и ТЩ алгоритм разработан автором.


Используя секвенциальные алгоритмы разрешимости и опираясь на оценки длины записи решений задачи целочисленного линейного программирования, можно дать и верхние оценки для теорий ЗЪ и 1Ъ . Но такая оценка превысит експоненту в степени полином четвертой степени, что является неприемлемых для практических целей. Поэтому, без уточнения оценок, в диссертации указывается, что такие алгоритмы УРтрудны и принадлежат классу РЯРАСЕ. В рассматриваемых в последующих главах логиках эти теории не используются. Для теории линейных неравенств Ъ2 И теории и, содержащей не более двух слагаемых в неравенстве, удается понизить верхнюю оценку сложности вывода до 2Сп если в каждом неравенстве используется не более одной переменной второе слагаемое, или оба слагаемых являются константами, или в неравенства только одно слагасхсое. Доказана теорема о том, что добавление сортов, то есть конечных носителей, не повысит верхних оценок сложности вывода во всех теориях. В заключение главы доказана Рполнота задачи выполнимости всех рассматриваемых теорий линейных неравенств. В главе 2 представлены три логики плюралистическая логика, смешанная логика Поста и смешанная логика Лукасевича Г лава содержит необходимые определения и построение секвенциальных исчислений для чистых секвенций, а также теоремы о семантической обоснованности исчислений. Плюралистическая логика основана на теории Цф, но содержит лишь не бо лее двух слагаемых в неравенстве. Особую семантику имеет ее подлогика эвристическая логика, в которой кортежи одержат по два элемента.