Метод резолюций и стратегии поиска опровержений

Татьяна Михайловна Леденева; Мария Владимировна Лещинская

doi:10.17308/sait.2021.1/3374

Татьяна Михайловна Леденева Воронежский государственный университет https://orcid.org/0000-0002-3944-2266
Мария Владимировна Лещинская Воронежский государственный университет https://orcid.org/0000-0001-6944-8485

DOI: https://doi.org/10.17308/sait.2021.1/3374

Ключевые слова: исчисление предикатов, метод резолюций, стратегии управления выводом

Аннотация

В статье предлагается новая стратегия управления выводом в методе резолюций для исчисления предикатов первого порядка. Данное исчисление является основой логической модели представления знаний, отличающейся высокой описательной мощностью. Используемое в исчислении предикатов понятие вывода на основе резолюции является максимально формализованным и эффективным. Логическая модель применима в основном в исследовательских системах, она предъявляет высокие требования и ограничения к предметной области. В статье приводятся основные сведения формальной теории предикатов первого порядка, описываются существующие стратегии и критерии, предлагаются новая стратегия и осуществляется ее сравнительный анализ с другими стратегиями. Ее отличительной особенностью является использование рейтингов, которые вычисляются для каждого дизъюнкта и учитывают его способность образовывать контрарную пару для порождения резольвенты. В статье приводятся алгоритмы, реализующие данную стратегию. Для сравнительного анализа стратегий используется ряд существующих стратегий и вводится новый критерий стратегии — количество дизъюнктов, многократно участвующих в построении резольвент.

Скачивания

Данные скачивания пока не доступны.

Биографии авторов

Татьяна Михайловна Леденева, Воронежский государственный университет

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

Мария Владимировна Лещинская, Воронежский государственный университет

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

Литература

1. Aho A., Ullman J. (1978) The theory of parsing, translation and compiling. Moscow : Mir.
2. Chen Ch., Li R. (1983) The mathematical logic and automated theorem proving. Moscow : Science.
3. Teise A. [et al.] (1990) A logical approach to artificial intelligence. T.1. From classical logic to logic programming. Moscow : Mir.
4. Baader F. (2003) The Description Logic Handbook. New York : Press of the Cambridge University.
5. Nilsson N. (1973) Artificial intelligence. Methods for finding solutions. Per. from English Stefanyuk V. L. Ed. Fomina S. V. Moscow : Mir. 272 p.
6. Maslov S. Yu. (1964) Backward method for establishing deducibility in the classical predicate calculus. SSS. Iss. 159, No 1. P. 17–20.
7. Ledeneva T. M., Aristova E. M. (2016) The formal axiomatic theories. Calculus of predicates. Part 1. Voronezh : Publishing House of the Voronezh State University.
8. Ledeneva T. M. (2020) The formal axiomatic theories. Calculus of predicates. Part 2. Voronezh : Publishing House of the Voronezh State University.
9. Pospelov D. A. (1990) Artificial intelligence. In 3 books. Book. 2. Models and Methods: Handbook. Ed. D. A. Pospelova. Moscow : Radio and communication. 304 p.
10. Novikov F. A. (2011) The systems of knowledge representation. St. Petersburg : Publishing House of the Polytechnic University.
11. Sowyer B., Foster D. (1986) Programming Expert Systems in Pascal. John Wiley & Sons, Inc. 198 p.
12. Maciol A. (2008) An application of rule based tool in attributive logic for business rules modeling // Expert Systems with Applications. April 2008. Vol. 34, No. 3. P. 1825–1836.
13. Robinson J. A. A Machine-Oriented Logic Based on the Resolution Principle // J. ACM.No 12.
14. Tyurin S. F., Gorodilov A. Yu. (2019) The features of logical inference in prolog programs // Bulletin of Perm University. Series: Mathematics. Mechanics. Computer science. No 3 (46). P. 91– 97.
15. Slagle J. (1967) Automatic theorem proving with renamable and semantic resolution // Journal of the Association for Computing Machinery. Vol. 14. P. 687–697.
16. Bratchikov I. L., Sazonova N. V. (2010) The formal-grammatical interpretation of logical inference. St. Petersburg, St. Petersburg Electrotechnical University “LETI” them. V. I. Ulyanov (Lenin). Computer tools in education, n. 6. P. 31–40.
17. Kasyanov V. N., Evstigneev V. A. (2003) The graphs in programming: processing, visualization and application. SPb. : BHV-Petersburg. 1104 p.