Курдюков Н.С.

Рязанский Государственный Радиотехнический Университет, Россия

АЛГОРИТМ ПРОВЕРКИ НЕПРОТИВОРЕЧИВОСТИ БАЗ ЗНАНИЙ SOA-СИСТЕМ

Для корректной работы алгоритмов логического анализа онтологической SOA-системы требуется проверять базу знаний на непротиворечивость[1].

Существует алгоритм Consistent[2], использующий сводимость к исчислению предикатов первого порядка. Алгоритм представлен на рисунке 1. Входным значением алгоритма является база знаний логики DL-Lite_R K=<T,A>, выходным значением является «истина», если база знаний K непротиворечива.

Далее описывается принцип работы алгоритма Consistent. Для перевода из утверждений в хранилище отрицательных включений cln(T)[2] к формулам исчисления предикатов первого порядка используется функция перевода δ[2]. Алгоритм Consistent вычисляет интерпретацию db(A)[2] и cln(T), извлекает над db(A) булевский запрос исчисления предикатов первого порядка, полученный посредством объединения всех формул исчисления предикатов первого порядка и возвращенных после применения функции δ к каждому утверждению в cln(T). Таким образом, в случае отсутствия отрицательных утверждений включения, входящих в К, q^db(A)_unsat = ⊥^db(A), где q_unsat – запрос проверяющий существование утверждений. Следовательно, Consistent(K) возвращает значение «истина».

Рисунок 1. Алгоритм Consistent

Когда K является противоречивой базой знаний, ответ на союз конъюнктивных запросов Q определяется как конечное множество кортежей[2], не являющееся достоверным ответом на запрос. Вследствие сказанного, перед использованием специфических алгоритмов логического анализа необходимо проверять базу знаний на непротиворечивость.

Вследствие того, что вложенность концептов C ⊑ D эквивалентна невыполнимости концепта C ⊓ ¬D, достаточно решение остальных задач сводить к задачам выполнимости[1].

Вследствие приводимости задач включения и проверки экземпляра к задачи проверки непротиворечивости базы знаний, показатель вычислительной сложности[3] для задачи проверки непротиворечивости базы знаний распространяется и на задачи включения и проверки экземпляра класса. Задача вложенности концептов или ролей находится в классе PTime[3] в зависимости от размера TBox. Задача проверки экземпляра находится в классе LogSpace[3] от размера ABox и в PTime в зависимости от размера всей базы знаний. Невысокий класс сложности доказывает эффективность алгоритма Consistent для проверки баз знаний SOA-систем на непротиворечивость.

Литература:

1. Baader F., Calvanese D., McGuinness D., Nardi D., Patel-Schneider P.F. The Description Logic Handbook: Theory, implementation, and applications. Cambridge University Press, 2nd edition, 2010. – 593 p.

2. Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Riccardo Rosati. Tractable Reasoning and Efficient Query Answering in Description Logics: The DL-Lite Family // Journal of Automated Reasoning, 2007. Vol. – 39(3). – P. 385 – 429.

3. Макконнелл Дж. Основы современных алгоритмов. 2-е дополненное издание // Москва: Техносфера, 2004. – 368с.