maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1052Research ArticleОригинальные статьиArticlesОб исчислении позитивно-образованных формул для автоматического доказательства теоремOn the calculus of positively constructed formulas for authomated theorem provingДавыдовА. В.DavydovA. V.artem@icc.ruЛарионовА. А.LarionovA. A.noemail@neicon.ruЧеркашинЕ. А.CherkashinE. A.noemail@neicon.ruИнститут динамики систем и теории управления СО РАН, г.ИркутскRussian FederationИнститут математики, экономики и информатики ИГУ, г.ИркутскRussian Federation2010201220101746069Copyright © Давыдов А.В., Ларионов А.А., Черкашин Е.А., 20102010Давыдов А.В., Ларионов А.А., Черкашин Е.А.Davydov A.V., Larionov A.A., Cherkashin E.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1052

Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как тйповые кванторы. Язык LF содержит всего два логических символа - для каждого и существует, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.

The paper deals with an expressive logic language LF and its calculus. Formulas of this language consist of some large-block structural elements, such as type quanti¯ers. The language LF contains only two logic symbols for any and is, which form the set of logic connectives of the language. A logic calculus JF and complete strategy for automated proof search based on a single unary rule of inference are considered. This calculus has a number of other features that lead to the reduction of combinatorial complexity of ¯nding the deductions in comparison with the known systems for automated theorem proving as the resolution method and Genzen calculus. Problems of effective implementation of JF as a program system for automated theorem proving are considered.

автоматическое доказательство теоремматематическая логиканеклассические логикиискусственный интеллектautomated theorem provingmathematical logicnonclassical logicsartificial intelligenceReferencesВасильев С.Н., Жерлов А.К., Федунов Е.А., Федосов Б.Е. Интеллектное управление динамическими системами. M.: Физматлит, 2000.Васильев С.Н., Жерлов А.К., Федунов Е.А., Федосов Б.Е. Интеллектное управление динамическими системами. M.: Физматлит, 2000.Жерлов А.К., Васильев С.Н. Исчисления позитивно-образованных формул // Актуальные проблемы информатики, прикладной математики и механики: Сб. научных трудов. Красноярск, 1996. Ч. 1. С. 44-56.Жерлов А.К., Васильев С.Н. Исчисления позитивно-образованных формул // Актуальные проблемы информатики, прикладной математики и механики: Сб. научных трудов. Красноярск, 1996. Ч. 1. С. 44-56.J.A. Robinson. A Machine-Oriented Logic Based on Resolution Principle // Journal of ACM. 1965. January. P. 23-41.J.A. Robinson. A Machine-Oriented Logic Based on Resolution Principle // Journal of ACM. 1965. January. P. 23-41.Peter Graf. Substitution Tree Indexing // Proceedings of the 6th International Conference on Rewriting Techniques and Applications. 1995. P. 117-131.Peter Graf. Substitution Tree Indexing // Proceedings of the 6th International Conference on Rewriting Techniques and Applications. 1995. P. 117-131.Stickel M. The path-indexing method for indexing terms // Technical Note 473, Artificial Intelligence Center, SRI International, RAVENSWOOD AVE., MENLO PARK, CA 94025Stickel M. The path-indexing method for indexing terms // Technical Note 473, Artificial Intelligence Center, SRI International, RAVENSWOOD AVE., MENLO PARK, CA 94025Черкашин Е.А. Разделяемые структуры данных в системе автоматического доказательства теорем КВАНТ/3 // Вычислительные технологии. 2008. Т. 13. С. 102-107.Черкашин Е.А. Разделяемые структуры данных в системе автоматического доказательства теорем КВАНТ/3 // Вычислительные технологии. 2008. Т. 13. С. 102-107.McCune W.W. Experiments with Discrimination-Tree indexing and Path Indexing for Term Retrieval // Journal of Automated Reasoning. 1992. V. 9(2). P. 147-167.McCune W.W. Experiments with Discrimination-Tree indexing and Path Indexing for Term Retrieval // Journal of Automated Reasoning. 1992. V. 9(2). P. 147-167.Давыдов А.В. Исчисление позитивно-образованных формул с функциональными символами // Прикладные алгоритмы в дискретном анализе: сб. науч. тр./ Под ред. д-ра физ.-мат. наук, проф. Ю.Д. Королькова. Иркутск : Изд-во Ир- кут. гос. Ун-та, 2008. 157 с. (Дискретный анализ и информатика, Вып. 2). C. 23-49.Давыдов А.В. Исчисление позитивно-образованных формул с функциональными символами // Прикладные алгоритмы в дискретном анализе: сб. науч. тр./ Под ред. д-ра физ.-мат. наук, проф. Ю.Д. Королькова. Иркутск : Изд-во Ир- кут. гос. Ун-та, 2008. 157 с. (Дискретный анализ и информатика, Вып. 2). C. 23-49.

The authors declare that there are no conflicts of interest present.