О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями

Abstract

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

Робота присвячена вивченню можливостей інтелектуальних систем, які надає деревовидна форма пошуку спростування при використанні резолюційної техніки, включаючи правила парамодуляційного типу. Розглядаються числення так званих літеральних дерев, які призначені для встановлення невиконання формул класичної логіки першого порядку як з рівністю, так і без неї. Наводяться результати про їх коректність та повноту.

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.