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



"Ч>

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

ГУЛЯМОВ Шухрат Баратович

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

05.13.11 -Математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

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

Иркутск -1997

Работа выполнена в Иркутском вычислительном центре Сибирского отделения Российской Академии наук

Научный руководитель: член-корреспондент РАН,

профессор С.Н. Васильев

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

профессор А.И. Москаленко кандидат технических наук, зав. лаб. И.В. Бычков

Ведущая организация: Вычислительный Центр РАН, г. Москва

Защита состоится "¡д_."_И ., 1997 г. в/¿Г часов на заседании диссертационного совета Д 003.64.01 в Иркутском вычислительном центре СО РАН по адресу:

664033, Иркутск, ул. Лермонтова, 134, зал заседаний Ученого совета

С диссертацией можно ознакомиться в библиотеке Иркутского вычислительного центра СО РАН.

Автореферат разослан _ШОЯЖШ1 г.

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

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

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

Ю. Ф. Орлов

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Менее традиционной считается проблематика машинного синтеза теорем, хотя она имеет также давнюю историю как и задачи автоматического доказательства теорем. Еще X. Вонг (Wang H.)1 и В.М. Глушков2 отмечали не меньшую значимость, хотя и большую трудность задачи автоматизации получения самих формулировок теорем.

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

Развертывание теории па основе ограничиваемого вывода впервые было апробировано на ЭВМ X. Вонгом в рамках секвенциального исчисления высказываний. В.М. Глушковым были предложены общие принципы саморазвития теории. Несколько промежуточное положение между задачами синтеза и доказательства теорем занимает задача корректирования недоказуемых гипотез. Подход к ее решению в исчислении высказываний предложен Г.В. Давыдовым.

Эффективным подходом к автоматизации синтеза и доказательства теорем в хорошо разработанных узких областях математических теорий является алгоритмизационный подход. Он основан на анализе техники формулировок и доказательств известных теорем рассматриваемой области. Основными достоинствами подхода являются меньшая комби-паторность вывода и большая понятность промежуточных результатов человеку по сравнению с ранее рассмотренными подходами. С использованием такого подхода В.М. Матросовым в динамике систем был пред-

1Воаг X. Напути к механической математике // Киберн. сб.-1962.- Т.5.- С.114-165.

2Глушков В.М. Машина доказывает. -М.: Знание, 1981. -64 с.

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

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

Методика исследований. Общая методика исследований состоит в применении современных методов математической логики и теории программирования.

Научная новизна. Результаты диссертации являются новыми.

Разработан новый алгоритм для согласования логических уравнений в дескриптивной семантике.

Предложен алгоритм построения формул связи в анализе управляемых систем.

Разработан метод решения логических уравнений в конструктивной семантике.

Создана система автоматического синтеза теорем (ACT) для ПЭВМ класса IBM AT.

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

Практическая значимость полученных результатов: Полученные результаты позволяют существенно расширить область применения методов синтеза теорем. Алгоритмы согласования логических уравнений позволяют расширить область применимости метода синтеза теорем в ма-

тематической теории систем. Алгоритмическое построение формул связи полезно для повышения степени автоматизированного синтеза теорем о динамических свойствах управляемых систем. Метод синтеза теорем в конструктивной семантике является хорошим инструментом в задачах планирования действий (вычислений и т.п.) Использование системы ACT позволяет существенно сократить время, затрачиваемое высококвалифицированными специалистами на получение формулировок теорем, а также повысить уровень интеллектуальности автоматических и автоматизированных систем в условиях неполноты информации и/или ограниченности ресурсов.

Апробация работы. Результаты диссертационной работы докладывались на Школах по пакетам прикладных программ (Иркутск, 1989, Адлер 1991), на Всесоюзных конференциях по прикладной логике (Новосибирск, 1985, 1988, 1992), на научной школе "Автоматизация создания математического обеспечения и архитектуры систем реального времени" (Иркутск, 1990), на Республиканском научно-техпическом семинаре "Машинные методы в задачах механики, устойчивости и управления" (Казань, 1990), на Всесоюзной научно-технической конференции "Интеллектуальные системы в машиностроении" (Самара, 1991), на Республиканской конференции "Современные проблемы алгоритмизации" (Ташкент, 1991), на Международном семинаре "Методы и программное обеспечение для автоматических управляемых систем" (Иркутск, 1991), на Всероссийской научной школе "Компьютерная логика, алгебра и интеллектное управление" (Иркутск, 1994).

Публикации. Основные результаты диссертации опубликовапы в 13 печатных работах.

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

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

Частным случаем рассматриваемых уравнений является уравнение:

к^А,кх -> Ат, (1)

где А] — известные формулы исчисления предикатов первого порядка, х — неизвестная формула того же языка, подлежащая отысканию с учетом следующих трудно формализуемых критериев нетривиальности: решение х должно быть по возможности 1) ближе к необходимым условиям и 2) легче проверяемо на моделях рассматриваемой прикладной теории, чем непосредственная проверка Ат.

Примером уравнения (1) в динамике систем и теории управления является уравнение:

М к V, кС V (2)

где: V — определение динамического свойства исходной математической модели 5 (изучаемой с точки зрения наличия в ней свойства "Р), ■Рс — определение аналогичного свойства в другой, вспомогательной, более простой по замыслу модели именуемой системой сравнения, М. — известное условие связи, накладываемое по определению на некоторые отображения, связывающие модели 5 и 5С,

С — неизвестная совокупность условий (одно или несколько), при выполнении которых в рассматриваемой теории справедлива импликация М. к Рс —* V. Примерами упомянутых отображений являются а) вектор-функции Ляпунова (ВФЛ) V : ТхХ —* Х£, где X и Хе — пространства состояний моделей 5 и 5С соответственно, Т — множество моментов времени3, б) гомоморфизмы (в случае динамических систем понимаемые в смысле БарбашинаД949 г.). Соответственно этим примерам а) и б) условие связи М может иметь смысл а') условие мажорирования

V* е Г У(*,а:(0) <*«(*)

значений ВФЛ V на процессах х модели 5 соответствующими процессами хс модели или б') условия преобразования процессов в процессы

\zteT У{1,хЩ = хс(1).

3Матросов В.М., Анапольский Л.Ю., Васильев С.Н. Метод сравнения в математической теории систем. - Новосибирск, Наука, 1980. 480 с.

Известные члены логических уравнений рассматриваются в языке позитивно-образованных формул, т.е. как первопорядковые формулы, построенные из тождественно истинных предикатов Р„ и тождественно ложных предикатов Рл с помощью логических связок конъюнкции & и дизъюнкции V и типовых кванторов (т-кванторов) wa. Общий вид т-кванторов wa £ {t&a, ша}:

= Vza(Za —),wa = 3za{Zak—),

где za — операторная переменная, Za - типовая формула (т-формула) соответствующего т-квантора. Частным случаем т-кванторов являются ограниченные кванторы, когда т-формулы Za имеют вид: za 6 М> где Mi некоторые фиксированные и непустые множества из описания рассматриваемой математической модели (например, Т,Х,ХС и т.д.).

Рассмотрим некоторый т-квантор wa € Ау Из аксиом рассматриваемой математической теории н т-формул, входящих в т-кванторы, которые управляют в записи формулы Aj рассматриваемым т-квантором wa, можно вывести факты za 6 М;. Эти множества М,- (одно или несколько) называются типами рассматриваемой переменной za.

Алгоритм решения первопорядковых логических уравнений4 предполагает так называемую согласованность известных членов уравнения. Этим обеспечивается существование подходящей графовой структуры решения х, в которую изоморфно были бы вложимы структуры известных членов уравнения. Ограничение класса допустимых решений формулами х такой структуры уменьшает комбинаторную сложность процесса синтеза решения, а также эвристически ориентирует его в направлении получения нетривиальных решений. Для расширения класса разрешимых по этому алгоритму уравнений предложен алгоритм согласования формул Aj,j = 1, т.

В его основе лежат предложенные автором идеи алгоритмического определения типов операторных переменных za и унификации обозначений некоторых однотипных переменных, т.е. имеющих некоторый общий тип Mi и входящих в разные формулы Aj,Ak,j к. Т-кванторы с унифицированными переменными упомянутым изоморфизмом переводятся в один и тот же т-квантор синтезируемого решения х ("склеиваются").

4Vassilyev S.N. Machine synthesis of mathematical theorems. - Logic Programming, 1990, v.9, JV2&3. - pp. 235-265.

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

Для уравнения (2) в динамике систем и теории управления предложен алгоритм построения формулы связи М по виду изучаемого свойства V (§3). Тем самым не только повышается степень автоматизации получения теорем типа теорем сравнения (теперь не надо задавать М в качестве исходных данных компьютерной программы), но и автоматически (в силу предложенного алгоритма построения /А) обеспечивается требование согласованности между собой известных членов уравнения. Предложенный алгоритм работоспособен в предположении, что определение ~РС аналогично V, а также, что определение V изучаемого динамического свойства содержит в качестве основных переменных начальный момент времени (¿о), текущий момент времени (¿), начальное состояние (хо), текущее состояние (х), управление (и), возмущение (р), движение (*).

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

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

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

где А,- (г = 1,гг) - попарно различные логические спецификации известных средств, Ап+1 - спецификация (постановка) задачи, X - решение логического уравнения, которое представляет собой искомое условие разрешимости задачи Ап+1 над набором средств (программ) Лг,..., Ап при следующих критериях допустимости решений X: решение X записано в сигнатуре известных членов уразнения и, что исключает тривиальные решения, по возможности должно быть логически слабее и не использовать априори отсутствующие реализации конструктивных кванторов существования из А„+1. Если в принимаемой семантнке логической истинности найденное условие X оказывается "тавтологией", то задача разрешима (тавтология недескриптивной формулы X понимается как общезначимость дескриптивной формулы Хл, полученной из X применением специального преобразования, называемого дескриптивизацией). В противном случае задача неразрешима и (по замыслу) X должно выражать условие ее разрешимости (иначе говоря, спецификацию недостающих средств или чисто дескриптивное условие).

Таким образом, в формулах А,- из (3) различаются дескриптивные и конструктивные т-кванторы, обозначаемые соответственно из* и из1^. В дальнейшем в этой главе считается, что позитивно-образованные формулы рассматриваемого языка не содержат структурных ветвлений (т.е. связок V). Если в А,- имеются кванторы то вместо обычной теоретическо-модельной семантики на универсуме О, используется следующая формула: формула Г называется выполнимой, если для каждого т-квантора 6 F можно конструктивно указать такую теоретико-множественную операциюда : О х ... х О —* Б, что Р1 выполнимо.

Задача Ап+1 разрешима над А,-, г = 1,п, и X, если каждому квантору хЬр из А„+1 можно поставить в соответствие такую композицию операций да из множества операций, отвечающих кванторам из Л,-, {= 11 п, и X, что для каждой интерпретации I' для &"=1А, &Х, в которой истинна формула А-'&Х^, формула истинна в интерпретации I, расширенной операциями <рр. Здесь I' — совокупность интерпретации I для формулы Г* вместе с операциями да для гЬ* 6 -Р. Здесь аргументами операций являются значения операторных переменных га конструктивных т-кванторов, управляющих т-квантором

Разрешение уравнения (3) сводится к последовательному разрешению уравнений

А^кХк ->■ Вк-1,

(4)

где Л;*, Вк-г- известные члены уравнения, X*- ищется, к > 1, г'ь € 1,п, Во = Ап+1, В* = Хк.

Доказана следующая теорема.

Теорема 1 . Всякое (формальное) решение Хк уравнения (4) является одновременно решением уравнения (3) (к = 1,2,...).

Способ построения Хк основан на "склейке" двух формул Л;* и Вк-ь Операцию склейки можно рассматривать как пополнение формулы Вц т-кванторами формулы А{к. При этом некоторые т-кванторы Л,-4 и В к-1 могут склеиться в один т-квантор.

Теорема 2 . Пусть Г - формула, построенная операцией склейки: Р -В * А. Тогда Р является решением логического уравнения А&.Х —► В.

Теорема 2 показывает, что операция склейки дает решение уравнения (4). Выделен подкласс общезначимых и. конструктивно распознаваемых формул, именуемых стоп-формулами.

Доказана следующая теорема о корректности алгоритма решения уравнения вида (3).

Теорема 3 . Если процесс построения Хк завершился синтезом стоп-формулы, то задача Лп+1 разрешима, над средствами А\,..., Ап.

В качестве применения метода решения логических уравнений рассматривается задача анализа сивтезируемости логических структур СБИС. Дано представление знаний в задачи проектирования логической схемы компаратора с заданной разрядностью и быстродействием. Схема приведена на рис. 1. При этом выделены следующие виды логических формул: спецификации параметризованных процедур для синтеза схемотехнического описания элементного базиса СБИС (например, таких, как инвертор, счетчик и т.д.) на специализированном языке; спецификации процедур, позволяющих поддерживать такие поведенческие понятия,как "согласование", "мажорирование* и т.д.; дескриптивные знания ( аксиомы типа некоторых неконструктивных утверждений, устанавливающих

Рис. 1: Схема компаратора с согласованием разрядности входов

отношения между понятиями рассматриваемой области); спецификация самого технического задания (ТЗ) на изготовление СБИС с заданными свойствами. Получены условия разрешимости задачи синтеза над конкретной совокупностью исходных процедур и знаний.

Аналогично, в задачи распознавания типа летательного аппарата формализуются не только сами распознаваемые объекты (их признаки, классы), но и функциональные возможности соответствующих технических средств (датчиков и т.д.), программных средства (программ, вычисляющих по одним признакам распознаваемого объекта другие признаки и др.) Формулы А\, ■ ■ -, Ап уравнения (3) при этом интерпретируются следующим образом :

• Формулы, описывающие классы распознаваемых объектов. Они утверждают о том, что если в распознаваемом объекте присутствуют определенные признаки (т.е., предикат, описывающий этот признак, принимает значение "истина"), то этот объект относится к . классу Пу;

в Формулы, устанавливающие отношения между признаками. Согласно этим формулам, если в распознаваемом объекте присутствуют признаки Р) 6 1, к, к - общее количество признаков), то в объекте присутствуют признаки Р\{1 6 ' ф Такие формулы являются только дескриптивными;

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

Формула Ап+1 является запросом в систему распознавания. Она содержит в себе уже известные признаки объекта, описание конкретной обстановки по распознаванию объекта и требует определить класс, которому он принадлежит. Получены условие разрешимости задачи распознавания типа летательного аппарата в разных частных случаях.

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

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

Система ACT имеет модульную организацию. В составе системы имеется восемь модулей: модуль синтаксического анализа известных членов уравнения и построения графов формул, модуль типизации переменных и согласование известных членов уравнения, модуль проверки согласованности известных членов уравнения, модуль решения логических уравнений в исчислении высказываний, модуль синтеза т-кванторов, логических связок формулы решения логического уравнепия, модуль построения графа решения логического уравнения, модуль формирования текста леммы сравнения, модуль формирования текста тесремы сравнения.

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

Управляющая программа системы ACT обеспечивает межмодульный интерфейс, управление файловой системой и интерфейс с пользователем.

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

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

Другие результаты машинных экспериментов с помощью системы "ACT" приведены в Приложении 1.

В заключении сформулированы основные результаты диссертацион-

ной работы.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

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

3. Создана система автоматического синтеза теорем (ACT) для ПЭВМ класса IBM AT, позволяющая сокращать время, затрачиваемое высококвалифицированными, специалистами на получение теорем, получения следствий или обзора гипотез.

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

По теме диссертации опубликованы следующие работы:

1. Васильев С.Н., Гулямов Ш.Б. Об одной задаче обзора непрямых следствий в динамике систем и теории управления // Всесоюзная конференция по прикладной логике. Новосибирск, 1985. - С. 33-35.

2. Васильев С.Н., Гулямов Ш.Б. Жерлов А.К., Литвинов Ю.Ф. Логический подход к автоматизации планирования решения задачи //II Всесоюзная конференция по прикладной логике, Новосибирск, 1988, с. 42.

3. Васильев С.Н., Гулямов Ш.Б. Жерлов А.К., Литвинов Ю.Ф. О логических средствах системы планирования вычисления "ПАСАД" // Алгоритмы, вып. 66, Ташкент, 1988, стр. 97-112.

4. Гулямов Ш.Б. Система автоматического синтеза теорем // Программное обеспечение ЭВМ новых поколений. Тезисы докладов VIII Сибирской школы по ППП, Иркутск 1989, с. 141.

5. Гулямов Ш.Б. Синтез теорем в задачах планирования // Автоматизация создания математического обеспечения и архитектуры СРВ, Тезисы докладов, Иркутск 1990, с. 24-25.

6. Васильев С.Н., Гулямов Ш.Б., Лакеев A.B., Чагина О.М. Пакет программ ACT в анализе сложных динамических свойств управляемых

систем // Машинные методы в задачах механики, устойчивости и управления. Тезисы докладов республиканского научно-технического семинара, Казань, 1990, с. 6.

7. Гулямов Ш.Б. Автоматизированный синтез теорем для проектирования СБИС // Интеллектуальные системы в машиностроении. Материалы Всесоюзной научно-технической конференции, Самара, 1991, часть 3, с. 73-76.

8. Гулямов Ш.Б. К автоматизации порождения условий разрешимости задач в ЭВМ // Современные проблемы алгоритмизации. Сборник тезисов, Ташкент, 1991, с. 116.

9. Guljamov Sh.B. Logic Equations in Constructive Semantics // IMACS/IFAC International Workshop. Methods and Software for Automatic Control Sytstems. Abstracts of Papers, Irkutsk, 1991 p. 87.

10. Гулямов Ш.Б. Синтез теорем в исчислении смешанной семантики // Программное обеспечение математического моделирования, управления и искусственного интеллекта. Тезисы IX школы по ППП, Иркутск 1991, с. 77.

11. Гулямов Ш.Б. Логические уравнения для задач распознавания образов // Логика и семантическое программирование. Вычислительные системы, 146, Новосибирск 1992, с. 147-148.

12. Гулямов Ш.Б. Метод решения логических уравнений в дескриптивно-конструктивной семантике. // Известия РАН. Сер. Теория и системы управления,- N 5, 1995, С. 24-37.

13. Гулямов Ш.Б. Применение метода синтеза теорем в задачах автоматического планирования // "Оптимизация, управление, интеллект", Иркутск, N 1, 1995, стр. 151-163.