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

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

Автор: Черкашин, Евгений Александрович

Шифр специальности: 05.13.11

Научная степень: Кандидатская

Год защиты: 1999

Место защиты: Иркутск

Количество страниц: 155 с. ил.

Артикул: 253725

Автор: Черкашин, Евгений Александрович

Стоимость: 250 руб.

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


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

Рекомендуемые диссертации данного раздела

28.06.2016

+ 100 бесплатных диссертаций

Дорогие друзья, в раздел "Бесплатные диссертации" добавлено 100 новых диссертаций. Желаем новых научных ...

15.02.2015

Добавлено 41611 диссертаций РГБ

В каталог сайта http://new-disser.ru добавлено новые диссертации РГБ 2013-2014 года. Желаем новых научных ...


Все новости

Время генерации: 0.197, запросов: 244