Об исчислении позитивно-образованных формул для автоматического доказательства теорем
Аннотация
Рассматривается выразительный логический язык LF и основанное на нем исчисление. Формулы этого языка состоят из некоторых крупно-блочных структурных элементов, таких как тйповые кванторы. Язык LF содержит всего два логических символа - для каждого и существует, которые составляют множество логических связок языка. Рассматривается логическое исчисление JF и полные стратегии автоматического поиска выводов, основанные на единственном унарном правиле вывода. Это исчисление обладает рядом других особенностей, благодаря которым достигается уменьшение комбинаторной сложности при поиске выводов в сравнении с такими известными системами автоматического доказательства теорем (АДТ), как метод резолюций и генценовские исчисления. Рассмотрены вопросы об эффективной реализации нового исчисления в виде программной системы для автоматического доказательства теорем.
Ключевые слова
автоматическое доказательство теорем,
математическая логика,
неклассические логики,
искусственный интеллект
MSC2020: 517.51+514.17
Об авторах
А. В. Давыдов
Институт динамики систем и теории управления СО РАН, г.Иркутск
Россия
Россия
А. А. Ларионов
Институт математики, экономики и информатики ИГУ, г.Иркутск
Россия
Россия
Е. А. Черкашин
Институт динамики систем и теории управления СО РАН, г.Иркутск
Россия
Россия
Список литературы
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.
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.)
Просмотров: 518
Послать статью по эл. почте 