Реферат: Удк 004. 89 Реализация системы логического вывода для логики первого порядка на базе структурных функциональных моделей

УДК 004.89


Реализация системы логического вывода для логики первого порядка на базе структурных функциональных моделей


Implementation of a first-order logic reasoner based on a structural functional model


Пинжин А.Е.

Email: alex_pinjin@tpu.ru


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

Стандартные машины вывода опираются на классический метод резолюций и различные его вариации [2]. Наиболее эффективным и часто используемым (особенно в зарубежных источниках) считается табличный (tableaux) метод, который позволяет добиться линейных затрат на осуществление вывода относительно объема исходной базы знаний [3]. Подход, представленный в [4, 5] предлагает альтернативный алгоритм вывода на основе теории структурных функциональных моделей (С-моделей) [6]. С-модель базируется на определении функциональной связи и изначально разрабатывалась для доказательства теорем с целью последующего синтеза структурных программ. В [7] показано, каким образом функциональные связи могут быть интерпретированы в виде дизъюнктов Хорна. Основной целью доклада является краткое обоснование применимости С-модели для различных логических исчислений: логики высказываний (ЛВ), логики первого порядка (ЛПП). Приведены результаты опытного сравнения производительности предлагаемого алгоритма с существующими реализациями.


^ Основные определения


Кратко перечислим основные определения, исходя из [6]:

Определение 1. Сигнатурой будем называть четверку =(A,F,P,D), где A, F, P и D – множества (элементарных) имен величин (атрибутов), функциональных символов, селекторных символов и имен схем, соответственно. Считается, что выделено непустое конечное подмножество ED имен примитивных или первичных схем (или типов).

Исходные данные для машины вывода поставляются в виде набора схем отношений. Для упрощения рассуждений будем рассматривать простые схемы без подсхем, вариантной части и рекурсивных вхождений.

Определение 2. Структурная функциональная модель (С-модель), представляет собой конечную совокупность схем М=(T1,…,Ts).

Определение 3. Простой схемой T объекта t будем называть выражение вида

T(t)=(T0(a0),T1(a1),…,Tn(an) | f_set), (1)

где T – имя схемы, a0,a1,…,an – собственные атрибуты (величины) схемы T; T0, T1,…,Tn  E – собственные (примитивные) подсхемы схемы T, определяющие тип соответствующих им атрибутов.

Выражение f_set в завершающей части описания схемы скрывает множество функциональных связей схемы T.


Определение 4. Функциональная связь (ФС) определяется выражением вида
f: a1,…,ana0, где f – имя, ai– аргументы, a0 – результат ФС. Функциональная связь входящая в схему Т, называется допустимой, если и только если a0,a1,…,an – собственные атрибуты схемы T. В дальнейшем будем рассматривать только синтаксически правильные схемы, где f_set содержит только допустимые ФС.

Постановка задачи планирования в С-модели М может быть представлена следующим образом:

S=(T(t),A0,X0), (2)

где t – непервичный атрибут схемы ТМ, на которой ставится задача, A0 и X0 – наборы имён соответственно исходных и искомых атрибутов, принадлежащих T.


^ Логика высказываний


Каждой (примитивной) величине aij ставится в соответствие примитивное высказывание Aij, а функциональный символ интерпретируется как знак логического следствия. Тогда множество ФС схемы может быть представлено в виде следующего выражения:

A0A01…A0n, …, AkAk…Akn,


либо в виде набора Хорновских дизьюнктов:


A0A01…A0n, …, AkAk…Akn (3)


Задача планирования (2), при A0 = {a1, …, ai}, X0 = {ai+1, …, aj}, для постановки задачи проверки выполнимости набора высказываний (sat-problem) интерпретируется как X0A0 , что, совместно с (3) соответствует:

A1 (4)

…

Ai

 Ai+1

…

 Aj

Приведенная интерпретация позволяет использовать алгоритмы вывода на С-модели для автоматического доказательства достаточно широкого множества теорем.


^ Логика первого порядка


Согласно [8] возможно приведение вывода высказываний логики первого порядка (ЛПП) к выводу в логике высказываний.

Приведем некоторый набор высказываний ЛПП, находящихся в стандартной форме и сформулируем задачу вывода:

z(A0(z)A01(z)…A0n(z), …, Ak(z)Ak(z)…Akn(z)

A1(z)

…

Ai(z)

 Ai+1(z)

…

 Aj(z))


Вполне очевидно, что пропозиционализация этих высказываний приводит теорему к виду (3, 4), а значит и к (2).


^ Экспериментальные результаты


Реализация машины вывода на С-модели подробно описана в [5]. Для целей сравнения были разработаны конвертеры формата данных С-модели в различные форматы [9–11], используемые машинами вывода, выбранными для сравнения. В приведенной ниже таблице приведен список реализаций машин вывода, вид логики и формат исходных данных:

Машина вывода

Логика

Формат данных

miniSat (sat4j)

ЛВ

cnf

Darwin 1.4.1

ЛПП

tme

paradox2.2

ЛПП

tptp-fof

iProver0.2

ЛПП

tptp-fof


Поясним выбор реализаций машин вывода. Пакет Sat4j содержит реализацию алгоритма miniSat, который показал максимальную производительность согласно итогам конкурса по решению SAT-проблемы в 2006 г. [12]. Darwin, Paradox, iProver– являются номинантами конкурса CADE ATP System Competition (CASC) 2007, проводимом ежегодно в рамках конференции по автоматизированному логическому выводу (Conference on automated deduction – CADE) [13]. Отметим, что реализацию Vampire 8.0, 9.1 не удалось задействовать по причине закрытого описания входных параметров.

Для целей сравнения выполнялась генерация и последующая конвертация схем числом ФС от 10 до 250 и равным количеством входных атрибутов. Аргументы и цели ФС связывались таким образом, чтобы обеспечить необходимость обработки всех элементов при осуществлении вывода.

Результаты испытаний приведены на рис. 1. Отметим, что при измерении времени работы алгоритмов на ЛПП учитывается время загрузки исходных данных, поэтому на графике а) результаты работы алгоритма вывода на С-модели отличаются от аналогичных результатов на б) и в).


а) б)




^ Рис. 1. Результаты сравнения производительности машин вывода

(а – на ЛВ, б – на ЛПП)


Заключение


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


Список источников


Berners-Lee T., Hendler J., Lassila O. The Semantic Web // Scientific American Magazine. –2001. – V. 284. – № 5. – P. 34–43.

Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. – М: Наука, 1983. – 358 c.

Baader F., Sattler U. An overview of tableau algorithms for description logics // Studia Logica. – 2000. – V. 69. – № 1. – P. 5–40.

Новосельцев В.Б. Синтез рекурсивных программ в системах управления пакетами прикладных программ: Дис. … канд. техн. наук. – Институт теоретической астрономии академии наук СССР. – Л., 1985. – 50 с.

Новосельцев В.Б., Пинжин А.Е. Реализация эффективного алгоритма синтеза линейных функциональных программ // Известия Томского политехнического университета. – 2008. – Т. 312. – № 5. – С. 32–35.

Новосельцев В.Б. Теория структурных функциональных моделей // Сибирский математический журнал. – 2006. – Т. 47. – № 5. – С. 1014–1030.

Новосельцев В.Б. Эффективный нерезолютивный вывод для ограниченного исчисления хорновских дизъюнктов // Известия Томского политехнического университета. – 2008. – Т. 312. – № 5. – С.32–36.

Рассел С., Норвиг П. Искусственный интеллект: современный подход (AIMA). 2-е изд. – Вильямс. – 2007. – С. 381–384.

SAT DIMACS Challenge – Satisfiability: Suggested Format [Электронный ресурс]. – 1993. – Режим доступа: ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/ satformat.tex.

TME input specification [Электронный ресурс]. – Режим доступа: http://www.uni-koblenz.de/ag-ki/Systems/Protein/tme-syntax.txt.

TPTP syntax v3.5.0 [Электронный ресурс]. – Режим доступа: http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html.

SAT-Race 2006: Runtime comparison of all SAT-Race solvers [Электронный ресурс]. – 2006. – Режим доступа: http://fmv.jku.at/sat-race-2006/analysis.html

The CADE ATP System Competition, part of the The 21st International Conference on Automated Deduction [Электронный ресурс]. – Bremen, Germany. – 17–20th July 2007. – Режим доступа: http://www.cs.miami.edu/~tptp/CASC/21/.