На правах рекламы:
ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Авторитетность издания

ВАК - К1
RSCI, ядро РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2024

В Московском государственном университете приборостроения и информатики предложен метод представления данных в логике предикатов первого порядка

20.07.2011

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

Этим требованиям удовлетворяет процедура вывода на графе связей Р. Ковальского, однако она имеет ряд существенных недостатков. Главный из них – значительные затраты вычислительных ресурсов и времени при его первоначальном создании. Особенно это касается огромных объемов данных. Кроме того, препроцессорная обработка множества дизъюнктов включена в саму процедуру вывода, что также отражается на вычислительной эффективности этой процедуры. Данный процесс должен быть вынесен за рамки процедуры вывода. Одним из способов решения является использование специальной структуры представления множества дизъюнктов.

Заметим, что препроцессорная обработка, осуществляемая на шаге инициализации множества дизъюнктов, не включает в себя предварительную обработку контрарных пар литер процедурой унификации. Ее включение в препроцессорную обработку позволит снизить вычислительное время основной работы процедуры вывода, так как каждая контрарная пара литер уже будет содержать предварительную информацию о множестве рассогласований подтермов. Для этого необходима разработка более производительного и эффективного алгоритма унификации, чем алгоритм, предложенный Дж. Робинсоном. Решением этой задачи является создание специальной структуры представления термов.

Подробное описание дается в статье «Метод дедуктивного вывода на семантических сетях концептуальных объектов», автор Раговский А.П. (Московский государственный университет приборостроения и информатики).