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

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

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

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2003
Автори: Асельдеров, З.М., Лялецкий, А.А.
Формат: Стаття
Мова:Russian
Опубліковано: Інститут проблем математичних машин і систем НАН України 2003
Теми:
Обчислювальні системи
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/726
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-726
record_format dspace
spelling irk-123456789-7262015-07-05T12:16:08Z Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции Асельдеров, З.М. Лялецкий, А.А. Обчислювальні системи Решается проблема построения эффективных целеориентированных секвенциальных исчислений для классической логики первого порядка (без равенства). Приводятся результаты об их корректности и полноте. Устанавливается связь этих исчислений с неполной в общем случае входной резолюцией, заданной в виде так называемой SLD-резолюции для деревьев специального вида (SLD-деревьев). Эта связь дает простой способ построения полного в общем случае расширения SLD-резолюции за счет добавления к SLD-резолюции так называемого правила контрарного закрытия, которое может быть легко запрограммировано в интеллектуальных системах, использующих SLD-технику и требующих её полного расширения на случай формул произвольного вида. Библиогр.: 11 назв. Вирішується проблема побудови ефективних цілеорієнтованих секвенційних числень для класичної логіки першого порядку (без рівності). Наводяться результати їх коректності та повноти. Встановлюється зв’язок цих числень зі вхідною резолюцією (яка є неповною у загальному випадку), що задана у вигляді SLD-резолюції для дерев спеціального вигляду (SLD-дерев). Цей зв’язок надає простий спосіб побудови повного у загальному випадку розширення SLD-резолюції за рахунок додання до SLD-резолюції так званого правила контрарного закриття, яке може бути легко запрограмоване в інтелектуальні системи, що використовують SLD-техніку та потребують її повного розширення на випадок формул довільного вигляду. Бібліогр.: 11 назв. The problem of the construction of effective goal-oriented calculi for first-order classical logic (without equality) is solved. Some results on soundness and completeness of the calculi are given. Their connection with the input resolution that is incomplete in general and has the form of the SLD-resolution for special trees (the SLD-trees) is fixed. The connection gives a simple way for the construction of a complete extension of the SLD-resolution by means of adding a so-called contrary-closing rule, which easily can be implemented in intelligent systems using SLD-technique and requiring its complete extension for sets of arbitrary formulas. Refs.: 11 titles. 2003 Article Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34. 1028-9763 http://dspace.nbuv.gov.ua/handle/123456789/726 518.74 ru Інститут проблем математичних машин і систем НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Russian
topic Обчислювальні системи
Обчислювальні системи
spellingShingle Обчислювальні системи
Обчислювальні системи
Асельдеров, З.М.
Лялецкий, А.А.
Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
description Решается проблема построения эффективных целеориентированных секвенциальных исчислений для классической логики первого порядка (без равенства). Приводятся результаты об их корректности и полноте. Устанавливается связь этих исчислений с неполной в общем случае входной резолюцией, заданной в виде так называемой SLD-резолюции для деревьев специального вида (SLD-деревьев). Эта связь дает простой способ построения полного в общем случае расширения SLD-резолюции за счет добавления к SLD-резолюции так называемого правила контрарного закрытия, которое может быть легко запрограммировано в интеллектуальных системах, использующих SLD-технику и требующих её полного расширения на случай формул произвольного вида. Библиогр.: 11 назв.
format Article
author Асельдеров, З.М.
Лялецкий, А.А.
author_facet Асельдеров, З.М.
Лялецкий, А.А.
author_sort Асельдеров, З.М.
title Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_short Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_full Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_fullStr Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_full_unstemmed Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_sort правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
publisher Інститут проблем математичних машин і систем НАН України
publishDate 2003
topic_facet Обчислювальні системи
url http://dspace.nbuv.gov.ua/handle/123456789/726
citation_txt Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34.
work_keys_str_mv AT aselʹderovzm pravilokontrarnogozakrytiâipolnyerasšireniâlogičeskogoapparataintellektualʹnyhsistemspravilomvhodnojrezolûcii
AT lâleckijaa pravilokontrarnogozakrytiâipolnyerasšireniâlogičeskogoapparataintellektualʹnyhsistemspravilomvhodnojrezolûcii
first_indexed 2025-07-02T04:23:01Z
last_indexed 2025-07-02T04:23:01Z
_version_ 1836507653980815360
fulltext ISSN 1028-9763. Математичні машини і системи, 2003, № 2 29 УДК 518.74 З.М. АСЕЛЬДЕРОВ, А.А. ЛЯЛЕЦКИЙ____________________________________________________ ПРАВИЛО КОНТРАРНОГО ЗАКРЫТИЯ И ПОЛНЫЕ РАСШИРЕНИЯ ЛОГИЧЕСКОГО АППАРАТА ИНТЕЛЛЕКТУАЛЬНЫХ СИСТЕМ С ПРАВИЛОМ ВХОДНОЙ РЕЗОЛЮЦИИ Введение Применение логики в интеллектуальных системах, как правило, предполагает создание и/или применение уже известных и достаточно эффективных методов поиска вывода в классической логике первого порядка. К числу последних относится входная резолюция, часто выбираемая в качестве базового дедуктивного аппарата разнообразных систем логического программирования. Для множеств хорновых дизъюнктов входная резолюция является корректным и полным методом, которая для достижения полноты в случае более широких классов дизъюнктов требует подключения дополнительных логических механизмов. Был получен ряд результатов [1–3] показывающих, что, в общем случае, за счет использования некоторой вспомогательной информации, можно получить полные расширения входной резолюции при построении линейных выводов. Параллельно, в целях повышения эффективности поиска вывода, изучался вопрос построения древовидного вывода с правилом входной резолюции. В результате входная резолюция приобрела вид так называемой SLD-резолюции, в ходе применения которой строятся SLD-деревья [4,5] и которая широко используется в интеллектуальных системах типа систем логического программирования. SLD-резолюция является корректной и полной для множеств хорновых дизъюнктов, но не сохраняет полноту для множеств произвольных дизъюнктов. Поскольку в текущее время стала актуальной способность интеллектуальных систем проводить формальные рассуждения, используя формулы произвольного вида, естественно, что возник вопрос о том, какими максимально простыми средствами необходимо дополнить SLD-резолюцию для получения полного метода поиска вывода в общем случае. Одно из возможных его решений предлагается в данной работе1: полное расширение SLD-резолюции достигается за счет встраивания в SLD-резолюцию достаточно простого правила вывода, названного здесь правилом контрарного закрытия. Специфической чертой данной работы является то, что упомянутое выше полное расширение SLD- резолюции появляется как «сужение» на дизъюнкты специальных машинно-ориентированных секвенциальных исчислений, разработанных в целях получения корректных и полных методов установления выводимости в классической логике первого порядка, которые, в некотором смысле, сравнимы по эффективности с широко используемыми резолюционными методами [6]. В этой связи секвенциальные исчисления, рассматриваемые здесь, могут выступать в качестве «естественных» полных расширений SLD-резолюции на секвенциальный случай. Сама же ориентация на развитие специальных секвенциальных исчислений была вызвана тем обстоятельством, что использование генценовского подхода [7] к проведению дедукции является намного более естественным и удобным при поиске доказательства, предусматривающего вмешательство человека в процесс дедукции. Заметим, что оптимизация перебора, возникающего из-за возможности разных порядков применения обычных кванторных правил, достигается в работе за счет предварительной сколемизации, впервые предложенной в [8] для формул первого порядка и позже перенесенной в [9] на секвенции. Современное состояние этих проблем подробно изложено в [10]. 1 Исследования, представленные в данной работе, поддержаны Intas-проектом 2000-447. ISSN 1028-9763. Математичні машини і системи, 2003, № 2 30 Предварительные сведения Рассматривается секвенциальная форма классической логики первого порядка без равенства. Известно [9], что установление выводимости любой секвенции может быть сведено к установлению подходящей замкнутой секвенции с элиминированными положительными кванторами. Следовательно, можно считать, что любая секвенция состоит из бескванторных формул, вместо переменных которых могут быть подставлены любые термы, а сами формулы секвенций попарно не имеют общих переменных. Считаются известными понятия литеры, терма, формулы и дизъюнкта. Если L – литера, то через L~ обозначается её дополнение. Выражение ¬F обозначает результат одношагового внесения отрицания в формулу F , а # – пустую формулу. Также отметим, что мы понимаем положительное [ ]( )+FP и отрицательное [ ]( )−FP вхождения формулы F в формулу P в обычном смысле. В дальнейшем будет использоваться определение (одновременного) наиболее общего унификатора в формулировке из [11]. Под равенством понимается упорядоченная пара термов s< , >t , записываемая в виде ts ≈ . Пусть L является литерой вида ( ) ( )( )nn ttRttR ,...,,..., 11 ¬ и M – литерой вида ( ) ( )( )nn ssRssR ,...,,..., 11 ¬ , где R есть предикатный символ и ,,...,1 ntt nss ,...,1 есть термы. Тогда через ( )ML,∑ обозначается множество равенств { }nn stst ≈≈ ,...,11 . В этом случае будем говорить, что литеры L и M являются эквивалентными по модулю ( ) ( )( )MLMLML ,mod, ∑≈∑ . Мы будем придерживаться обычного понятия секвенции. Формулы из антецедента секвенции будут называться ее посылками, а формулы из сукцедента – ее целями. В дальнейшем будут рассматриваться только секвенции с одной целью в сукцеденте секвенции. При этом понятие секвенции распространяется на выражения вида #→Г , где # обозначает пустую формулу. Секвенции #→Г будут называться аксиомами рассматриваемых секвенциальных исчислений. Деревья понимаются в обычном смысле. Деревья растут «сверху вниз». В дальнейшем мы будем рассматривать так называемые секвенциальные деревья. Секвенциальное дерево – это дерево, каждая вершина которого помечена некоторой секвенцией. Часто вершина дерева будет отождествляться с секвенцией, приписанной ей в качестве метки. В процессе поиска вывода начальной секвенции S строится так называемое дерево вывода Tr относительно S . В начальный момент процесса поиска дерево Tr состоит только из корня, помеченного S , и называется инициальным деревом. Если на некотором этапе Tr уже сгенерировано, то последующие вершины дерева порождаются в соответствии с тем или иным правилом вывода, примененным к некоторому листу Tr в случае, когда такое применение правила возможно. С каждым деревом вывода связывается специальное множество равенств ( )TrEq . ( )TrEq полагается равным пустому множеству ∅ для каждого инициального дерева вывода. Если же дерево вывода Tr отлично от инициального, то ( )TrEq полагается равным ( ) ( )MLTrEq ,' ∑∪ , где 'Tr – такое дерево вывода, что Tr «выводится» из 'Tr применением некоторого подходящего правила вывода, генерирующим соответствующее ( )ML,∑ (см. ниже). ISSN 1028-9763. Математичні машини і системи, 2003, № 2 31 Дерево вывода Tr относительно секвенции S называется деревом доказательства относительно S тогда и только тогда, когда каждый лист Tr помечен аксиомой и существует одновременный наиболее общий унификатор всех равенств из ( )TrEq . Пусть nPP ...,1 и G есть формулы ( )0≥n , и S обозначает секвенцию GPP n →...,1 . Тогда формульным образом ( )Sϕ называется формула GPP n ⊃∧∧ ...1 , когда 0>n , и ( )Sϕ есть G , когда 0=n . Если G есть # , то ( )Sϕ есть # . Заметим, что # всегда полагается общезначимой формулой. Целеориентированное исчисление секвенций Описываемое ниже исчисление GS предназначено для установления того, что формула G является логическим следствием формул nPP ...,1 (в этом случае nPP ...,1 и G называются инициальными формулами). Ясно, что для задания GS нам требуется только определить его правила вывода. 1. Правила расщепления цели. Эти правила предназначены для элиминации главной логической связки рассматриваемой цели. Результатом применения каждого такого правила является новая секвенция (секвенции) с новой целью (целями) и, возможно, новыми посылками. Отметим, каждое правило расщепления цели генерирует ( )ML,∑ , равное пустому множеству ∅ . ; , GFГ GFГ → ⊃→ ; , FGГ GFГ → ⊃→ ¬ ; , GFГ GFГ → ∨→ ¬ ; , FGГ GFГ → ∨→ ¬ ; GFГГ GFГ →→ ∧→ ¬→ ¬→ FГ FГ . 2. Правило дублирования посылки. [ ] [ ] LГMFFГ LГMFГ → → + + 2 ' 1 21 ,,, ,, , где ( )MLML ,mod∑≈ и 'F есть вариант формулы F . 3. Правила расщепления цели. Порядок применения правил этого типа “управляется” литерой L из сукцедента. Отметим, что везде ниже M обозначает литеру, удовлетворяющую условию: ( )MLML ,mod∑≈ . [ ] [ ]( ) ; ,,, ,, 2121 21 ¬¬+ − →→ →⊃ GГГГГMFГ LГGMFГ [ ] [ ]( ) ; ,,, ,, 2121 21 FГГГГMGГ LГMGFГ →→ →⊃ ¬+ + [ ] [ ] ; ,,, ,, 2121 21 FГLГГMGГ LГMGFГ ¬→→ →∨ + + [ ] [ ] ; ,,, ,, 2121 21 GГLГГMFГ LГGMFГ ¬→→ →∨ + + [ ] [ ] ; ,,, ,, 21 21 LГFMGГ LГMGFГ → →∧ + + [ ] [ ] ; ,,, ,, 21 21 LГGMFГ LГGMFГ → →∧ + + ISSN 1028-9763. Математичні машини і системи, 2003, № 2 32 [ ]( ) [ ] ; ,, ,, 21 11 LMF LГMFГ →∆∆ →¬ +¬ − . #,, ,, 21 21 → → ГMГ LГMГ 4. Правило контрарного закрытия (CC-правило). Пусть Tr – некоторое дерево вывода и Br – его ветвь с листом Lf , помеченная секвенцией LГ → , где Г – последовательность формул и L – литера. Пусть ветвь Br содержит секвенцию MГ →' , где ' Г является последовательностью формул и M – такая литера, что ( )MLML ,~mod~ ∑≈ . Если дерево 'Tr получено из Tr с помощью присоединения к Lf одного наследника, помеченного секвенцией #→Г , то говорится, что 'Tr выводимо из Tr с помощью правила контрарного закрытия (СС-правила). При этом множество ( )'TrEq определяется равным ( ) ( )MLTrEg ,~∑∪ . Относительно исчисления GS имеет место следующее утверждение. ПРЕДЛОЖЕНИЕ 1. Пусть формулы nPP ,...,1 образуют конечное непротиворечивое множество формул. Тогда формула G является логическим следствием формул nPP ,...,1 в том и только том случае, когда существует дерево доказательства относительно секвенции GGPP n →¬,,...,1 в исчислении GS . Схема доказательства. Прежде всего заметим, что теорема Эрбрана в формулировке работы [9] и некоторые другие результаты из [9] позволяют ограничиться рассмотрением только пропозиционального случая выводимости в исчислении GS , т.е. рассмотрением только таких деревьев вывода Tr , у которых ( ) ∅=∑ Tr . Для пропозиционального случая полнота исчисления GS может быть доказана индукцией по числу бинарных логических связок в инициальной секвенции, исследуемой на выводимость, а корректность может быть легко проверена с помощью понятия формульного образа ( )Sϕ секвенции .... DEQS Модификации исчисления GS Отдельного обсуждения заслуживает случай, когда мы рассматриваем секвенции вида kmnnr LLMMMM ∧∧→∨∨∨∨ ............ 1,1,,1,11,1 , где kmn LLMM ,...,,,..., 1,1,1 – литеры. Поскольку каждая формула первого порядка может быть приведена к конъюнктивной (дизъюнктивной) нормальной форме такими преобразованиями, которые сохраняют логическую эквивалентность, то на основании результатов из [9] легко показать, что установление выводимости любой секвенции произвольного вида эквивалентно установлению выводимости некоторой подходящей секвенции вида kmnnr LLMMMM ∧∧→∨∨∨∨ ......,...,... 1,1,1,11,1 . Вот почему в данном разделе мы рассматриваем только секвенции такого вида. В этой связи отметим, что если G есть kLL ∧∧ ...1 , то ¬G есть k1 L~...~ ∨∨L . Учитывая вышесказанное, исчисление GS может быть трансформировано в исчисление LS “литеральных” секвенций, которое имеет следующие правила: 1. Правило расщепления цели. Приводимое ниже правило обобщает правило “расщепления конъюнкции в цели” исчисления GS , если рассматривать ∧ как многоместную операцию: ISSN 1028-9763. Математичні машини і системи, 2003, № 2 33 . ,..., ... 1 m m LГLГ LLГ →→ ∧∧→ 2. Правило расщепления посылки. Это правило может быть применено, когда цель рассматриваемой секвенции является литерой: ''' 1 '''' 1 ' 2111 ,...,,,..., ,......, rn rn BГBГAГAГ LГBBMААГ −→−→−→−→ →∨∨∨∨∨∨ , где ,,...,,,..., 11 rn BBAA L и M – литеры, ( )MLML ,mod∑≈ и ',...,,,..., ' 1 '' 1 rn BBAA – новые варианты литер rn BBAA ,...,,,..., 11 соответственно и ' Г является последовательностью 2111 ,......, ГBBMААГ rn ∨∨∨∨∨∨ . Исчисление LS имеет такое же # -правило и CC-правило, как и исчисление GS . ПРЕДЛОЖЕНИЕ 2. Пусть дизъюнкты nРР ,...,1 образуют конечное непротиворечивое множество дизъюнктов. Конъюнкция литер G является логическим следствием дизъюнктов nРР ,...,1 в том и только том случае, когда существует дерево доказательства относительно секвенции nРР ,...,1 , GG →¬ в исчислении LS . Схема доказательства. В соответствии с предложением 1, существует дерево доказательства Tr относительно секвенции nРР ,...,1 , GG →¬ в исчислении GS . Очевидно, что Tr содержит применение только таких правил вывода исчисления GS , которые имеют соответствующие аналоги в исчислении .... DEQLS Особенностью исчисления LS является то, что антецеденты выводимых секвенций совпадают с антецедентом соответствующей инициальной секвенции. Это позволяет рассматривать антецедент этой инициальной секвенции как множество входных дизъюнктов и преобразовывать каждое дерево вывода Tr исчисления LS в дерево ( )Trγ , листья которого совпадают с листьями дерева Tr , и помеченное целями соответствующих секвенций (и только ими). Мы будем называть такое дерево ( )Trγ деревом целей, соответствующим дереву Tr . Таким образом, имеется простой способ перехода от исчисления LS к SLD- резолюции. Полнота SLD-резолюции для множеств хорновых дизъюнктов является известным результатом логического программирования. Следующее предложение содержит его. СЛЕДСТВИЕ (корректность и полнота SLD-резолюции). Пусть nРР ,...,1 являются положительными хорновыми дизъюнктами, и G является конъюнкцией атомарных формул. ЦельG является логическим следствием дизъюнктов nРР ,...,1 в том и только в том случае, когда существует дерево доказательства относительно секвенции GРР n →,...,1 в исчислении LS (без применений CC-правила). Доказательство. В соответствии с предложением 2 существует дерево доказательства Tr относительно секвенции nРР ,...,1 , GG →¬ в исчислении LS . Очевидно, что Tr не содержит секвенций, ISSN 1028-9763. Математичні машини і системи, 2003, № 2 34 выводимых по CC-правилу. Следовательно, ( )σγ Tr является SLD-деревом, где σ есть одновременный наиболее общий унификатор всех равенств из ( )TrEq . ... DEQ Выводы Полученные результаты показывают, что исчисление LS даёт способы построения полных расширений SLD- резолюции для множеств дизъюнктов произвольного вида посредством встраивания в SLD-резолюцию правила контрарного закрытия или его аналогов. Если же мы интересуемся возможностями полного расширения SLD-резолюции на случай установления выводимости секвенций с произвольными формулами, то можно воспользоваться различными модификациями исчисления GS . Эти свойства исчислений GS и LS определяют методы модификации программных средств в целях получения полных в общем случае расширений логического аппарата разнообразных интеллектуальных систем (например, экспертных систем, систем логического программирования, дедуктивных баз данных и т.д.), использующих SLD-резолюцию в качестве базовой техники поиска логического вывода. СПИСОК ЛИТЕРАТУРЫ 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 с.

Схожі ресурси