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

УДК 518.74

З.М. АСЕЛЬДЕРОВ, А.А. ЛЯЛЕЦКИЙ

ПРАВИЛО КОНТРАРНОГО ЗАКРЫТИЯ И ПОЛНЫЕ РАСШИРЕНИЯ ЛОГИЧЕСКОГО АППАРАТА ИНТЕЛЛЕКТУАЛЬНЫХ СИСТЕМ С ПРАВИЛОМ ВХОДНОЙ РЕЗОЛЮЦИИ

Введение

Применение логики в интеллектуальных системах, как правило, предполагает создание и/или применение уже известных и достаточно эффективных методов поиска вывода в классической логике первого порядка. К числу последних относится входная резолюция, часто выбираемая в качестве базового дедуктивного аппарата разнообразных систем логического программирования. Для множеств хорновых дизъюнктов входная резолюция является корректным и полным методом, которая для достижения полноты в случае более широких классов дизъюнктов требует подключения дополнительных логических механизмов. Был получен ряд результатов [1-3] показывающих, что, в общем случае, за счет использования некоторой вспомогательной информации, можно получить полные расширения входной резолюции при построении линейных выводов.

Параллельно, в целях повышения эффективности поиска вывода, изучался вопрос построения древовидного вывода с правилом входной резолюции. В результате входная резолюция приобрела вид так называемой ЭШ-резолюции, в ходе применения которой строятся ЭШ-деревья [4,5] и которая широко используется в интеллектуальных системах типа систем логического программирования. ЭШ-резолюция является корректной и полной для множеств хорновых дизъюнктов, но не сохраняет полноту для множеств произвольных дизъюнктов. Поскольку в текущее время стала актуальной способность интеллектуальных систем проводить формальные рассуждения, используя формулы произвольного вида, естественно, что возник вопрос о том, какими максимально простыми средствами необходимо дополнить ЭШ-резолюцию для получения полного метода поиска вывода в общем случае. Одно из возможных его решений предлагается в данной работе1: полное расширение ЭЮ-резолюции достигается за счет встраивания в ЭШ-резолюцию достаточно простого правила вывода, названного здесь правилом контрарного закрытия.

Специфической чертой данной работы является то, что упомянутое выше полное расширение ЭШ-резолюции появляется как «сужение» на дизъюнкты специальных машинно-ориентированных секвенциальных исчислений, разработанных в целях получения корректных и полных методов установления выводимости в классической логике первого порядка, которые, в некотором смысле, сравнимы по эффективности с широко используемыми резолюционными методами [6]. В этой связи секвенциальные исчисления, рассматриваемые здесь, могут выступать в качестве «естественных» полных расширений ЭЮ-резолюции на секвенциальный случай. Сама же ориентация на развитие специальных секвенциальных исчислений была вызвана тем обстоятельством, что использование генценовского подхода [7] к проведению дедукции является намного более естественным и удобным при поиске доказательства, предусматривающего вмешательство человека в процесс дедукции. Заметим, что оптимизация перебора, возникающего из-за возможности разных порядков применения обычных кванторных правил, достигается в работе за счет предварительной сколемизации, впервые предложенной в [8] для формул первого порядка и позже перенесенной в [9] на секвенции. Современное состояние этих проблем подробно изложено в [10].

1 Исследования, представленные в данной работе, поддержаны Intas-проектом 2000-447. ISSN 1028-9763. Математичн машини i системи, 2003, № 2

Предварительные сведения

Рассматривается секвенциальная форма классической логики первого порядка без равенства. Известно [9], что установление выводимости любой секвенции может быть сведено к установлению подходящей замкнутой секвенции с элиминированными положительными кванторами. Следовательно, можно считать, что любая секвенция состоит из бескванторных формул, вместо переменных которых могут быть подставлены любые термы, а сами формулы секвенций попарно не имеют общих переменных.

Считаются известными понятия литеры, терма, формулы и дизъюнкта. Если Ь - литера, то через ~ Ь обозначается её дополнение. Выражение Е0 обозначает результат одношагового внесения отрицания в формулу Е , а # - пустую формулу. Также отметим, что мы понимаем положительное (р[е + ]) и

отрицательное (р[е"]) вхождения формулы Е в формулу Р в обычном смысле.

В дальнейшем будет использоваться определение (одновременного) наиболее общего унификатора в формулировке из [11]. Под равенством понимается упорядоченная пара термов < 5 , ^ >, записываемая в виде 5 » ^.

Пусть Ь является литерой вида , 1П)(—Я(^,..., 1П)) и М - литерой вида

Я^,..., 5п)(—Я^,..., 5п)), где Я есть предикатный символ и 1П, 51,..., 5п есть термы. Тогда через ^(Ь,М) обозначается множество равенств {^ » 51,..., 1п » 5п}. В этом случае будем говорить, что литеры Ь и М являются эквивалентными по модулю

Е(Ь, М )(Ь » М то а е(ь, М)).

Мы будем придерживаться обычного понятия секвенции. Формулы из антецедента секвенции будут называться ее посылками, а формулы из сукцедента - ее целями.

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

Деревья понимаются в обычном смысле. Деревья растут «сверху вниз». В дальнейшем мы будем рассматривать так называемые секвенциальные деревья. Секвенциальное дерево - это дерево, каждая вершина которого помечена некоторой секвенцией. Часто вершина дерева будет отождествляться с секвенцией, приписанной ей в качестве метки.

В процессе поиска вывода начальной секвенции S строится так называемое дерево вывода Тг относительно S . В начальный момент процесса поиска дерево Тг состоит только из корня, помеченного S ,

и называется инициальным деревом. Если на некотором этапе Тг уже сгенерировано, то последующие вершины дерева порождаются в соответствии с тем или иным правилом вывода, примененным к некоторому листу Тг в случае, когда такое применение правила возможно.

С каждым деревом вывода связывается специальное множество равенств Ец(Тг). Ец(Тг) полагается равным пустому множеству 0 для каждого инициального дерева вывода. Если же дерево вывода Тг отлично от инициального, то

Ед(Тг) полагается равным Ед(Тг )и Е(Ь,М), где Тг ' - такое дерево

вывода, что Тг «выводится» из Тг' применением некоторого подходящего правила вывода, генерирующим соответствующее

Е(Ь, М) (см. ниже).

Дерево вывода Тг относительно секвенции S называется деревом доказательства относительно S тогда и только тогда, когда каждый лист Тг помечен аксиомой и существует одновременный наиболее общий унификатор всех равенств из Ед(Тг).

Пусть Рп и О есть формулы (п > 0), и $ обозначает секвенцию Рп  О . Тогда формульным образом р($) называется формула Р1 А ... А Рп 3 О , когда п > 0, и р($) есть О , когда п = 0. Если О есть # , то р($) есть # . Заметим, что # всегда полагается общезначимой формулой.

Целеориентированное исчисление секвенций

Описываемое ниже исчисление О$ предназначено для установления того, что формула О является логическим следствием формул Р1...,Рп (в этом случае Р1...,Рп и О называются инициальными

формулами). Ясно, что для задания О$ нам требуется только определить его правила вывода.

1. Правила расщепления цели. Эти правила предназначены для элиминации главной логической связки рассматриваемой цели. Результатом применения каждого такого правила является новая секвенция (секвенции) с новой целью (целями) и, возможно, новыми посылками. Отметим, каждое правило расщепления

цели генерирует !(А М), равное пустому множеству 0.

Г  ^ з О Г  ^ з О

Г, F  G '

Г  F v G; Г, F 0  G'

Г  F a G ; Г  Fr  G1

Г, G 0  F

Г  F v G Г, G 0  F

Г 0F Г  F0 '

2. Правило дублирования посылки.

Г„ F M +1Г2  L Г1, F', FIM+1Г2  L '

где L » M mo d Z(L, M) и F есть вариант формулы F .

3. Правила расщепления цели. Порядок применения правил этого типа "управляется" литерой L из сукцедента. Отметим, что везде ниже M обозначает литеру, удовлетворяющую условию: L » M mod Z(L,M).

Г1,F[MG,Г2  L

2  ГГ1, Г 2  G -

Г1, (f [m+])0, Г

Г1, F v G[M+1Г2  L Г1,G[M +_[ Г2  L^, Г2  0F

Г1,F a GM+1Г2  L ; Г1, G[M+1F, Г2  L '

Г1, F 3 GM+1Г2  L Г1, (g\m+])0, г2  ГГ1, Г2  F

Г1,F[M+]vG,Г2 L ; Г1, F [m+] Г2  Lr 1, Г2  0G'

Г1,F|M+]a G,Г2  L ; Г1, F [M +1G, Г2  L '

Г1, —(е [М " ]) Г1  Ь ; Г1, М, Г 2  Ь А1, Е0 М+ ] А 2  Ь ' Г1, М, Г2

4. Правило контрарного закрытия (СС-правило). Пусть Тг - некоторое дерево вывода и Вг - его ветвь с листом Ь/ , помеченная секвенцией Г  Ь , где Г - последовательность формул и Ь - литера.

Пусть ветвь Вг содержит секвенцию Г  М, где Г является последовательностью формул и М -

такая литера, что ~ Ь » МтоёЬ,М). Если дерево Тг получено из Тг с помощью присоединения к

Ь/ одного наследника, помеченного секвенцией Г , то говорится, что Тг выводимо из Тг с помощью

правила контрарного закрытия (СС-правила). При этом множество Ец(Гг ) определяется равным

Eg(Тг)и Е(~ Ь,М).

Относительно исчисления ОБ имеет место следующее утверждение.

ПРЕДЛОЖЕНИЕ 1. Пусть формулы Р1,...,Рп образуют конечное непротиворечивое множество формул. Тогда формула О является логическим следствием формул Р1,... , Рп в том и только том случае,

когда существует дерево доказательства относительно секвенции Р1,..., Рп, —О  О в исчислении ОБ .

Схема доказательства. Прежде всего заметим, что теорема Эрбрана в формулировке работы [9] и некоторые другие результаты из [9] позволяют ограничиться рассмотрением только пропозиционального случая выводимости в исчислении ОБ, т.е. рассмотрением только таких деревьев вывода Тг, у которых ^(Тг) = 0 . Для пропозиционального случая полнота исчисления ОБ может быть доказана индукцией по числу бинарных логических связок в инициальной секвенции, исследуемой на выводимость, а корректность может быть легко проверена с помощью понятия формульного образа р(Б) секвенции Б^.Е.О.

Модификации исчисления ОБ

Отдельного обсуждения заслуживает случай, когда мы рассматриваем секвенции вида Мц V ... VМ1г1,..Мп1 V ... VМпм  Ь1 А ... А Ьк, где Ми,...,Мпт,Ь1,...,Ьк - литеры. Поскольку

каждая формула первого порядка может быть приведена к конъюнктивной (дизъюнктивной) нормальной форме такими преобразованиями, которые сохраняют логическую эквивалентность, то на основании результатов из [9] легко показать, что установление выводимости любой секвенции произвольного вида эквивалентно установлению выводимости некоторой подходящей секвенции вида

М11 V ... V М1 г1,...,Мп 1 V ... V Мп т  Ь1 А... А Ьк. Вот почему в данном разделе мы рассматриваем только секвенции такого вида. В этой связи отметим, что если О есть Ь1 А... А Ьк, то О— есть ~ Ь1 V ...V ~ Ьк.

Учитывая вышесказанное, исчисление ОБ может быть трансформировано в исчисление ЬБ "литеральных" секвенций, которое имеет следующие правила:

1. Правило расщепления цели. Приводимое ниже правило обобщает правило "расщепления конъюнкции в цели" исчисления ОБ , если рассматривать А как многоместную операцию:

Г  Ь А ... А ьт Г  Ь1,..., Г  Ьт

2. Правило расщепления посылки. Это правило может быть применено, когда цель рассматриваемой секвенции является литерой:

Г,, Д V... V А V М V В1 V... V В, Г2  Ь

1 5 1 п 1 г 5 2

Г ,..., г' -Ап , г' -в1 ,..., Г ~ВГ

где А1,..., Ап,В1,...,Вг, Ь и М - литеры, Ь »Мто а Е(Ь, М) и А1 ,..., Ап ,В1 ,...,Вг' - новые варианты литер А1,..., Ап,В1,...,Вг соответственно и Г является последовательностью Г1, А1 V... V Ап VМ V В1 V... V Вг, Г2.

Исчисление Ь$ имеет такое же # -правило и СС-правило, как и исчисление О$ . ПРЕДЛОЖЕНИЕ 2. Пусть дизъюнкты Р1,...,Рп образуют конечное непротиворечивое множество

дизъюнктов. Конъюнкция литер О является логическим следствием дизъюнктов Р1,...,Рп в том и только том случае, когда существует дерево доказательства относительно секвенции Р1,...,Рп , О0  О в исчислении Ь$ .

Схема доказательства. В соответствии с предложением 1, существует дерево доказательства Тг относительно секвенции Р1,...,Рп , О0  О в исчислении О$. Очевидно, что Тг содержит применение только таких правил вывода исчисления О$, которые имеют соответствующие аналоги в исчислении

Ь$ .0.Е.£.

Особенностью исчисления Ь$ является то, что антецеденты выводимых секвенций совпадают с антецедентом соответствующей инициальной секвенции. Это позволяет рассматривать антецедент этой инициальной секвенции как множество входных дизъюнктов и преобразовывать каждое дерево вывода Тг исчисления Ь$ в дерево у(Тг), листья которого совпадают с листьями дерева Тг, и помеченное целями

соответствующих секвенций (и только ими). Мы будем называть такое дерево у(Тг) деревом целей,

соответствующим дереву Тг. Таким образом, имеется простой способ перехода от исчисления Ь$ к БШ-резолюции.

Полнота ЭЮ-резолюции для множеств хорновых дизъюнктов является известным результатом логического программирования. Следующее предложение содержит его.

СЛЕДСТВИЕ (корректность и полнота БЬй-резолюции). Пусть Р1,...,Рп являются положительными

хорновыми дизъюнктами, и О является конъюнкцией атомарных формул. Цель О является логическим

следствием дизъюнктов Р1,... , Рп в том и только в том случае, когда существует дерево доказательства

относительно секвенции Р1,...,Рп  О в исчислении Ь$ (без применений СС-правила).

Доказательство. В соответствии с предложением 2 существует дерево доказательства Тг относительно секвенции Р1,..., Рп , О0  О в исчислении Ь$ . Очевидно, что Тг не содержит секвенций,

выводимых по СС-правилу. Следовательно, у\Тг )О является ЭЮ-деревом, где О есть одновременный наиболее общий унификатор всех равенств из Ед(Тг). 0.ЕХ».

Выводы

Полученные результаты показывают, что исчисление ЬБ даёт способы построения полных расширений ЭШ-резолюции для множеств дизъюнктов произвольного вида посредством встраивания в ЭЮ-резолюцию правила контрарного закрытия или его аналогов. Если же мы интересуемся возможностями полного расширения ЭЮ-резолюции на случай установления выводимости секвенций с произвольными формулами, то можно воспользоваться различными модификациями исчисления ОБ. Эти свойства исчислений ОБ и ЬБ определяют методы модификации программных средств в целях получения полных в общем случае расширений логического аппарата разнообразных интеллектуальных систем (например, экспертных систем, систем логического программирования, дедуктивных баз данных и т.д.), использующих ЭЮ-резолюцию в качестве базовой техники поиска логического вывода.

СПИСОК ЛИТЕРАТУРЫ

1. Pool D.L., Goeble R. Gracefully Adding Negation and Disjunction to Prolog // Lecture Notes in Computer Science. - 1986. - Vol. 220. - P. 635 - 641.

2. Stickel M. A. Prolog Technology Theorem Prover // New Generation Comp. - 1984. - Vol. 4. - P. 371 - 383.

3. Stickel M. A. Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler // Lecture Notes in Computer Science. - 1986. - Vol. 232. - P. 573 - 587.

4. Apt K.R., van Emden M. H. Contributions into the Theory of Logic Programming // JASM. - 1982. - Vol. 3, N 29. - P. 841 - 862.

5. Lloyd J.V. Foundations of Logic Programming. - Berlin, 1987. - 476 p.

6. Robinson J. A machine-oriented logic based on resolution principle // Journal of the ACM. - 1965. - Vol. 12, N 1. - P. 23 - 41.

7. Gentzen G. Untersuchungen uber das Logische Schliessen // Math. Z. - 1934. - Vol. 39. - P. 176 - 210.

8. Skolem T. Logisch-kombinatorische Untersuchungen uber die Erfullbarkeit oder Beweisbarkeit mathematischer Satze // Skriftner utgit ar Videnskapsselskaper i Kristiania. - 1920. - Vol. 4. - P. 4 - 36.

9. Минц Г.Е. Теорема Эбрана // Математическая теория логического вывода. - М.: Наука, 1967. - С. 311 - 350.

10. Handbook of Automated Reasoning. - Elsevier Science Publishers, 2001. - Vol. 1: Edited by A.Robinson and A.Voronkov. -1020 p.

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