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

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

Full description

Saved in:
Bibliographic Details
Date:2003
Main Authors: Асельдеров, З.М., Лялецкий, А.А.
Format: Article
Language:Russian
Published: Інститут проблем математичних машин і систем НАН України 2003
Subjects:
Online Access:https://nasplib.isofts.kiev.ua/handle/123456789/726
Tags: Add Tag
No Tags, Be the first to tag this record!
Journal Title:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-726
record_format dspace
spelling Асельдеров, З.М.
Лялецкий, А.А.
2008-06-24T13:27:58Z
2008-06-24T13:27:58Z
2003
Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34.
1028-9763
https://nasplib.isofts.kiev.ua/handle/123456789/726
518.74
Решается проблема построения эффективных целеориентированных секвенциальных исчислений для классической логики первого порядка (без равенства). Приводятся результаты об их корректности и полноте. Устанавливается связь этих исчислений с неполной в общем случае входной резолюцией, заданной в виде так называемой 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.
ru
Інститут проблем математичних машин і систем НАН України
Обчислювальні системи
Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
Правило контрарного закриття та повні розширення логічного апарату інтелектуальних систем з правилом вхідної резолюції
Contrary-closing rule and complete extensions of the logical technique of the intellectual systems with the input resolution rule
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
spellingShingle Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
Асельдеров, З.М.
Лялецкий, А.А.
Обчислювальні системи
title_short Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_full Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_fullStr Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_full_unstemmed Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
title_sort правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции
author Асельдеров, З.М.
Лялецкий, А.А.
author_facet Асельдеров, З.М.
Лялецкий, А.А.
topic Обчислювальні системи
topic_facet Обчислювальні системи
publishDate 2003
language Russian
publisher Інститут проблем математичних машин і систем НАН України
format Article
title_alt Правило контрарного закриття та повні розширення логічного апарату інтелектуальних систем з правилом вхідної резолюції
Contrary-closing rule and complete extensions of the logical technique of the intellectual systems with the input resolution rule
description Решается проблема построения эффективных целеориентированных секвенциальных исчислений для классической логики первого порядка (без равенства). Приводятся результаты об их корректности и полноте. Устанавливается связь этих исчислений с неполной в общем случае входной резолюцией, заданной в виде так называемой 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.
issn 1028-9763
url https://nasplib.isofts.kiev.ua/handle/123456789/726
citation_txt Правило контрарного закрытия и полные расширения логического аппарата интеллектуальных систем с правилом входной резолюции / З.М. Асельдеров, А.А. Лялецкий // Математические машины и системы. – 2003. – № 2. – C. 29-34.
work_keys_str_mv AT aselʹderovzm pravilokontrarnogozakrytiâipolnyerasšireniâlogičeskogoapparataintellektualʹnyhsistemspravilomvhodnoirezolûcii
AT lâleckiiaa pravilokontrarnogozakrytiâipolnyerasšireniâlogičeskogoapparataintellektualʹnyhsistemspravilomvhodnoirezolûcii
AT aselʹderovzm pravilokontrarnogozakrittâtapovnírozširennâlogíčnogoaparatuíntelektualʹnihsistemzpravilomvhídnoírezolûcíí
AT lâleckiiaa pravilokontrarnogozakrittâtapovnírozširennâlogíčnogoaparatuíntelektualʹnihsistemzpravilomvhídnoírezolûcíí
AT aselʹderovzm contraryclosingruleandcompleteextensionsofthelogicaltechniqueoftheintellectualsystemswiththeinputresolutionrule
AT lâleckiiaa contraryclosingruleandcompleteextensionsofthelogicaltechniqueoftheintellectualsystemswiththeinputresolutionrule
first_indexed 2025-12-07T15:26:31Z
last_indexed 2025-12-07T15:26:31Z
_version_ 1850863718154371073