Машины логического вывода на основе теории параллельных дедуктивных и абдуктивных вычислений

Машины логического вывода на основе теории параллельных дедуктивных и абдуктивных вычислений

Автор: Страбыкин, Дмитрий Алексеевич

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

Научная степень: Докторская

Год защиты: 1999

Место защиты: Киров

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

Артикул: 292621

Автор: Страбыкин, Дмитрий Алексеевич

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

Машины логического вывода на основе теории параллельных дедуктивных и абдуктивных вычислений  Машины логического вывода на основе теории параллельных дедуктивных и абдуктивных вычислений 

ВВЕДЕНИЕ. Машины логического вывода. Формальные системы и методы. Исходный базис. Основные теоремы и производные правила вывода. Вывод логических следствий. Методы резолюции и деления дизъюнктов. Задача абдуктивного вывода. Исчисление предикатов 1Р. Исходный базис. Унификация литералов. Базовый метод дедуктивного вывода7 8
2. Частичное деление дизъюнктов. Базовая процедура вывода. Базовый метод вывода. Эффективность метода. Модифицированное частичное деление дизъюнктов. Модифицированное полное деление дизъюнктов. Обобщенная процедура вывода. Метод параллельного абдуктивного вывода. Краткая характеристика. Параллельные логические вычисления. АЛОГ4
й1ЬЬ. Цу. V . Мх новое множество дизъюнктов исходных секвенций т новое множество дизъюнктов выводимых секвенций. I, иначе сразу устанавливается признак ц1. В ДДпроцедуре выполняются следующие действия. Все дизъюнкты исходных секвенций делятся на дизъюнкт выводимой секвенции Ь1гс1, ,. Выражение дЬх иО упрощается путем перемножения
дизъюнктов и исключения конъюнкций, содержащих сомножители вида ЬЬОЬ, и производится проверка не является ли это выражение теоремой исчисления I.


I, иначе сразу устанавливается признак ц1. В ДДпроцедуре выполняются следующие действия. Все дизъюнкты исходных секвенций делятся на дизъюнкт выводимой секвенции Ь1гс1, ,. Выражение дЬх иО упрощается путем перемножения
дизъюнктов и исключения конъюнкций, содержащих сомножители вида ЬЬОЬ, и производится проверка не является ли это выражение теоремой исчисления I. Если преобразуемая таким образом секвенция оказывается теоремой исчисления I ОюО, то вывод успешно завершается 0 и производится переход к п. Х1 vX2V . XV . Хр1 0 , в которой Хр4 . Полученные таким образом секвенции в соответствии со вторым условием правила предположения П7 рассматриваются как новые выводимые секвенции и их дизъюнкты включаются в множество ш. Устанавливается значение признака окончания вывода . Формируется новое множество дизъюнктов исходных секвенций Мх М М0, где М0 подмножество дизъюнктов множества М, для которых выполняется условие Э Г С1 Ф 1. Конец процедуры. Метод вывода. Логический вывод следствий методом деления дизъюнктов заключается в многократном применении ДДпроцедур и состоит из ряда шагов. На каждом шаге вывода ДДпроцедуры применяются к имеющимся выводимым и соответствующим им исходным дизъюнктам, образуя новые выводимые и новые исходные дизъюнкты, используемые на следующем шаге. Процесс вывода заканчивается, когда на очередном шаге обнаруживается дизъюнкт, для которого вывод не возможен , или для всех, выводимых на данном шаге дизъюнктов, будут сформированы признаки успешного завершения вывода д0.

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

28.06.2016

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

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

15.02.2015

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

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


Все новости

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