On the calculus of positively constructed formulas for authomated theorem proving
Abstract
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.
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.
About the Authors
A. V. Davydov
Институт динамики систем и теории управления СО РАН, г.Иркутск
Russian Federation
Russian Federation
A. A. Larionov
Институт математики, экономики и информатики ИГУ, г.Иркутск
Russian Federation
Russian Federation
E. A. Cherkashin
Институт динамики систем и теории управления СО РАН, г.Иркутск
Russian Federation
Russian Federation
References
1. Васильев С.Н., Жерлов А.К., Федунов Е.А., Федосов Б.Е. Интеллектное управление динамическими системами. M.: Физматлит, 2000.
2. Жерлов А.К., Васильев С.Н. Исчисления позитивно-образованных формул // Актуальные проблемы информатики, прикладной математики и механики: Сб. научных трудов. Красноярск, 1996. Ч. 1. С. 44-56.
3. J.A. Robinson. A Machine-Oriented Logic Based on Resolution Principle // Journal of ACM. 1965. January. P. 23-41.
4. Peter Graf. Substitution Tree Indexing // Proceedings of the 6th International Conference on Rewriting Techniques and Applications. 1995. P. 117-131.
5. Stickel M. The path-indexing method for indexing terms // Technical Note 473, Artificial Intelligence Center, SRI International, RAVENSWOOD AVE., MENLO PARK, CA 94025
6. Черкашин Е.А. Разделяемые структуры данных в системе автоматического доказательства теорем КВАНТ/3 // Вычислительные технологии. 2008. Т. 13. С. 102-107.
7. 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.
8. Давыдов А.В. Исчисление позитивно-образованных формул с функциональными символами // Прикладные алгоритмы в дискретном анализе: сб. науч. тр./ Под ред. д-ра физ.-мат. наук, проф. Ю.Д. Королькова. Иркутск : Изд-во Ир- кут. гос. Ун-та, 2008. 157 с. (Дискретный анализ и информатика, Вып. 2). C. 23-49.
Review
For citations:
Davydov A.V., Larionov A.A., Cherkashin E.A. On the calculus of positively constructed formulas for authomated theorem proving. Modeling and Analysis of Information Systems. 2010;17(4):60-69. (In Russ.)
Views:
557
Email this article 