О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями
Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для...
Збережено в:
Дата: | 2010 |
---|---|
Автор: | |
Формат: | Стаття |
Мова: | Russian |
Опубліковано: |
Інститут проблем математичних машин і систем НАН України
2010
|
Назва видання: | Математичні машини і системи |
Теми: | |
Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/47360 |
Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
Цитувати: | О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraineid |
irk-123456789-47360 |
---|---|
record_format |
dspace |
spelling |
irk-123456789-473602013-07-13T03:03:24Z О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями Афонин, А.А. Нові інформаційні і телекомунікаційні технології Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для установления невыполнимости формул классической логики первого порядка как с равенством, так и без него. Приводятся результаты об их корректности и полноте. Робота присвячена вивченню можливостей інтелектуальних систем, які надає деревовидна форма пошуку спростування при використанні резолюційної техніки, включаючи правила парамодуляційного типу. Розглядаються числення так званих літеральних дерев, які призначені для встановлення невиконання формул класичної логіки першого порядку як з рівністю, так і без неї. Наводяться результати про їх коректність та повноту. The paper is devoted to the study of intelligent system possibilities given by the tree-like form of refutation search when using the resolution technique with paramodulation-type rules. Calculation of so-called literal trees intended for the establishment of formula unsatisfiability of first-order classic logic, both with equality and without it, are considered. Results about their correctness and completeness are given. 2010 Article О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. 1028-9763 http://dspace.nbuv.gov.ua/handle/123456789/47360 004.89:510.649 ru Математичні машини і системи Інститут проблем математичних машин і систем НАН України |
institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
collection |
DSpace DC |
language |
Russian |
topic |
Нові інформаційні і телекомунікаційні технології Нові інформаційні і телекомунікаційні технології |
spellingShingle |
Нові інформаційні і телекомунікаційні технології Нові інформаційні і телекомунікаційні технології Афонин, А.А. О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями Математичні машини і системи |
description |
Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для установления невыполнимости формул классической логики первого порядка как с равенством, так и без него. Приводятся результаты об их корректности и полноте. |
format |
Article |
author |
Афонин, А.А. |
author_facet |
Афонин, А.А. |
author_sort |
Афонин, А.А. |
title |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
title_short |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
title_full |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
title_fullStr |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
title_full_unstemmed |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
title_sort |
о древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями |
publisher |
Інститут проблем математичних машин і систем НАН України |
publishDate |
2010 |
topic_facet |
Нові інформаційні і телекомунікаційні технології |
url |
http://dspace.nbuv.gov.ua/handle/123456789/47360 |
citation_txt |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. |
series |
Математичні машини і системи |
work_keys_str_mv |
AT afoninaa odrevovidnojformepoiskaoproverženiâvintellektualʹnyhsistemahslogičeskimivozmožnostâmi |
first_indexed |
2023-10-18T18:07:18Z |
last_indexed |
2023-10-18T18:07:18Z |
_version_ |
1796143367906656256 |