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

• Автор: Страбыкин, Дмитрий Алексеевич
• Шифр специальности: 05.13.13, 05.13.11
• Научная степень: Докторская
• Год защиты: 1999
• Место защиты: Киров
• Количество страниц: 415 с. : ил.

ВВЕДЕНИЕ. Машины логического вывода. Формальные системы и методы. Исходный базис. Основные теоремы и производные правила вывода. Вывод логических следствий. Методы резолюции и деления дизъюнктов. Задача абдуктивного вывода. Исчисление предикатов 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.