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


https://doi.org/10.18255/1818-1015-2010-4-60-69

Полный текст:


Аннотация

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

Об авторах

А. В. Давыдов
Институт динамики систем и теории управления СО РАН, г.Иркутск
Россия


А. А. Ларионов
Институт математики, экономики и информатики ИГУ, г.Иркутск
Россия


Е. А. Черкашин
Институт динамики систем и теории управления СО РАН, г.Иркутск
Россия


Список литературы

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.


Дополнительные файлы

Для цитирования: Давыдов А.В., Ларионов А.А., Черкашин Е.А. Об исчислении позитивно-образованных формул для автоматического доказательства теорем. Моделирование и анализ информационных систем. 2010;17(4):60-69. https://doi.org/10.18255/1818-1015-2010-4-60-69

For citation: 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.) https://doi.org/10.18255/1818-1015-2010-4-60-69

Просмотров: 4

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)