Соболь Александр Михайлович - магистр физикоматематических наук, аспирант кафедры интеллектуальных систем, факультет радиофизики и компьютерных технологий.
Ул. Курчатова, 5, 220064, Минск
AlexanderM. Sobol - M. Sci. (Phys.-Math.), Postgraduate Student, Department of Intelligent Systems, Faculty of Radiophysics and Computer Technologies.
St. Kurchatova, 5, 220064, Minsk
Козлова Елена Ивановна 0 кандидат физико-математических наук, доцент, заведующий кафедрой интеллектуальных систем, факультет радиофизики и компьютерных технологий.
Ул. Курчатова, 5, 220064, Минск
Elena I. Kozlova - Cand. Sci. (Phys.-Math.), Head of the Department of Intelligent Systems, Faculty of Radiophysics and Computer Technologies.
St. Kurchatova, 5, 220064, Minsk
Чернявский Юрий Александрович - кандидат технических наук, доцент кафедры информатики, факультет компьютерных систем и сетей.
Ул. П. Бровки, 6, 220013, Минск
Yuri A. Chernyavsky - Cand. Sci. (Eng.), Associate Professor of the Department of Informatics, Faculty of Computer Systems and Networks.
St. P. Brovki, 6, 220013, Minsk
Известны три основных семейства алгоритмов вывода в логике первого порядка: прямой логический вывод и его применение к дедуктивным базам данных и продукционным системам; процедуры обратного логического вывода и системы логического программирования; системы доказательства теорем на основе метода резолюции. При решении конкретных проблем наиболее эффективными являются алгоритмы, позволяющие охватить все факты и аксиомы, которые должны быть учтены в процессе логического вывода. Рассматривается пример применения логики первого порядка с целью выявления виновных в противоправных действиях. На основании высказываний формируется база знаний из выражений, с помощью которых составляется выражение логики первого порядка. Приводятся доказательства рассуждений, полученных в прямом логическом выводе с помощью дерева доказательств. Прямой логический вывод предусматривает выполнение допустимых этапов логического вывода на основе всех известных фактов, поэтому также рассматривается метод на основе резолюции при реализации обратного логического вывода с учетом выражения, полученного при прямом логическом выводе. Данное выражение преобразуется в конъюнктивную нормальную формулу с помощью законов булевой алгебры и доказывается методом исключения событий с помощью операции конъюнкции.
There are three main families of inference algorithms in first-order logic: direct inference and its application to deductive databases and production systems; backward inference procedures and logic programming systems; theorem proving systems based on the resolution method. When solving specific problems, the most effective algorithms are those that allow you to cover all the facts and axioms and must be taken into account in the process of inference. An example is considered in which it is necessary to prove the guilt of a person in murder. On the basis of statements, a knowledge base is formed from expressions, with the help of which an expression of first-order logic is compiled and proved using direct logical inference. The proof of the reasoning obtained in direct inference using the proof tree is given. However, direct inference provides for the implementation of all admissible stages of logical inference based on all known facts. The article also considers a method based on the resolution when implementing the reverse inference, taking into account the expression obtained in the direct inference. This expression is converted into a conjunctive normal formula using the laws of Boolean algebra and is proved by the elimination of events using the conjunction operation.
The authors declare that there are no conflicts of interest present.