Натуральный вывод для системы логики линейного времени
##plugins.themes.bootstrap3.article.sidebar##
Published:
16.01.2007
##plugins.themes.bootstrap3.article.main##
Abstract
We present a sound and complete Quine-style natural deduction system for propositional linear-time temporal logic based on similar systems for the propositional classical logic. The presented system can serve as a basis for the construction of provers, which are of interest in the context of research in Artificial Intelligence.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Bolotov A., Bashukovski A., Grigoriev O., Shangin V. Натуральный вывод для системы логики линейного времени // Logicheskie Issledovaniya / Logical Investigations. 2007. VOL. 13. C. 71-94.
Issue
Section
Papers
References
Болотов А.Е., Бочаров В.А., Горчаков А. А., Макаров В.В., Шангин В.О. Пусть докажет компьютер. М.: Наука, 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.
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.