Натуральный вывод для системы логики линейного времени

Main Article Content

А.Е. Болотов
А. Бащуковски
О.М. Григорьев
В.О. Шангин

Аннотация

Мы представляем непротиворечивую и полную систему натурального вывода в стиле Куайна для пропозициональной линейной временной темпоральной логики, основанной на аналогичных системах для пропозициональной классической логики. Представленная система может служить основой для построения пруверов, которые представляют интерес в контексте исследований в области искусственного интеллекта.

Скачивания

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

Article Details

Как цитировать
Болотов А., Бащуковски А., Григорьев О., Шангин В. Натуральный вывод для системы логики линейного времени // Логические исследования / Logical Investigations. 2007. Т. 13. C. 71-94.
Выпуск
Раздел
Статьи

Литература

Болотов А.Е., Бочаров В.А., Горчаков А. А., Макаров В.В., Шангин В.О. Пусть докажет компьютер. М.: Наука, 2004.
Gentzen G. Investigation into Logical Deduction, The Collected Papers of Gerhard Gentzen. Amsterdam. North-Holland, 1969. P. 68-131.
Gabbay D., Phueli A., Shelah S., and Stavi J. On the temporal analysis of fairness. // Proceedings of 7th ACM Symposium on Principles of Programming Languages. 1980. P. 163-173.
Fitch F. Symbolic Logic. NY, Roland Press, 1952.
Quine W. On natural deduction. // Journal of Symbolic Logic. V. 15. 1950. P. 93-102.
Fisher M., Dixon C., and Peim M. Clausal Temporal Resolution. // ACM Transactions on Computational Logic (TOCL). V. 1. № 2. 2001. P. 12-56.
Marchignoli D. Natural Deduction Systems for Temporal Logic. Department of Informatics, Unviersity of Pisa. 2002.
Simpson A. The Proof Theory and Semantics of Intuitionistic Modal Logic. College of Science and Engineering, School of Informatics, University of Edinburgh, 1994.