О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями
Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для...
Gespeichert in:
| Veröffentlicht in: | Математичні машини і системи |
|---|---|
| Datum: | 2010 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут проблем математичних машин і систем НАН України
2010
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/47360 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-47360 |
|---|---|
| record_format |
dspace |
| spelling |
Афонин, А.А. 2013-07-12T09:23:35Z 2013-07-12T09:23:35Z 2010 О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/47360 004.89:510.649 Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для установления невыполнимости формул классической логики первого порядка как с равенством, так и без него. Приводятся результаты об их корректности и полноте. Робота присвячена вивченню можливостей інтелектуальних систем, які надає деревовидна форма пошуку спростування при використанні резолюційної техніки, включаючи правила парамодуляційного типу. Розглядаються числення так званих літеральних дерев, які призначені для встановлення невиконання формул класичної логіки першого порядку як з рівністю, так і без неї. Наводяться результати про їх коректність та повноту. 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. ru Інститут проблем математичних машин і систем НАН України Математичні машини і системи Нові інформаційні і телекомунікаційні технології О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями Про деревовидну форму пошуку спростування в інтелектуальних системах з логічними можливостями Tree-like form of refutation search in intelligent systems with logic possibilities 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 |
2010 |
| language |
Russian |
| container_title |
Математичні машини і системи |
| publisher |
Інститут проблем математичних машин і систем НАН України |
| format |
Article |
| title_alt |
Про деревовидну форму пошуку спростування в інтелектуальних системах з логічними можливостями Tree-like form of refutation search in intelligent systems with logic possibilities |
| description |
Работа посвящена изучению возможностей интеллектуальных систем, которые предоставляет древовидная форма поиска опровержения в спучае использования резолюционной техники, включая правила парамодуляционного типа. Рассматриваются исчисления так называемых литеральных деревьев, которые предназначены для установления невыполнимости формул классической логики первого порядка как с равенством, так и без него. Приводятся результаты об их корректности и полноте.
Робота присвячена вивченню можливостей інтелектуальних систем, які надає деревовидна форма пошуку спростування при використанні резолюційної техніки, включаючи правила парамодуляційного типу. Розглядаються числення так званих літеральних дерев, які призначені для встановлення невиконання формул класичної логіки першого порядку як з рівністю, так і без неї. Наводяться результати про їх коректність та повноту.
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.
|
| issn |
1028-9763 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/47360 |
| citation_txt |
О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями / А.А. Афонин // Мат. машини і системи. — 2010. — № 1. — С. 87-94. — Бібліогр.: 13 назв. — рос. |
| work_keys_str_mv |
AT afoninaa odrevovidnoiformepoiskaoproverženiâvintellektualʹnyhsistemahslogičeskimivozmožnostâmi AT afoninaa proderevovidnuformupošukusprostuvannâvíntelektualʹnihsistemahzlogíčnimimožlivostâmi AT afoninaa treelikeformofrefutationsearchinintelligentsystemswithlogicpossibilities |
| first_indexed |
2025-11-27T11:06:04Z |
| last_indexed |
2025-11-27T11:06:04Z |
| _version_ |
1850852150066806784 |