Программная система КВАНТ/1 для автоматического доказательства теорем

• Автор: Черкашин, Евгений Александрович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Иркутск
• Количество страниц: 155 с. : ил.

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


Процесс поиска опровержения поформулы обладает естественным ИЛИ,паралеллизмом, т. ЭВМ I8 и I9 архитектурами. Аббрев. Ii Много инструкций мпого данных. Аббрев. Ii Одна инструкция много данных
простота понимания и интерпретации полученного вывода человеком. Применение логического исчисления , имеющего дескриптивную семантику, т. ЭВМ, автоматическое управление и т. Вообще, сама применимость логического подхода к задачам на конструктивный поиск построение объектов, удовлетворяющих конкретным требованиям, обычно предполагает построение специальных логических исчислений с конструктивной семантикой. При этом, например, выводимость формулы А В может пониматься как разрешимость задачи достижения цели В с помощью средств А и из конструктивного вывода формулы А В извлекаются требуемые конструкции планы, программы, управление и т. Оказывается , довольно широкий класс формул вида А В, где А, В Ь, обладает свойством конструктивности их дескриптивных выводов. ЗТ УХЛ 1. Вп. Теорема 1. Если В принадлежит классу 1. Формула В строится из формулы В путем инверсии знаков кванторов в каждой вершине дерева, добавления вершины УТ в виде нового корня дерева, а к каждой листовой вершине новой вершины ЗЕ. Теорема 1. В из класса 1. Предметом исследования диссертационной работы является программная система АДТ КВАНТ1, реализующая алгоритмы доказательства в исчислении поформул , , а также демонстрация решения задач, в том числе задач управления, требующих конструктивного вывода, с помощью этой программы.