Система интерактивного доказательства теорем.
##plugins.themes.bootstrap3.article.sidebar##
Published:
04.11.1993
##plugins.themes.bootstrap3.article.main##
Abstract
В настоящей статье списана система интерактивного поиска доказательства Deductio. Она позволяет строить доказательства, гарантируя их корректность. При этом пользователю доступны различные средства автоматизации.
Подобного рода проекты активно развиваются сейчас в различных научных центрах. Но описываемая здесь система обладает той особенностью, что она рассчитана на работу не с одной какой-либо логической системой, а с довольно широким их классом. Для этого используется специальный язык описания логических систем. И как только некоторая логическая система описана в терминах этого языка, она поддерживается программой.
Описываемая здесь система реализована для IBM PC совместимых компьютеров. Разработка осуществлена при содействии Института Логики, Когнитологии и Развития Личности. В ней, кроме автора настоящей статьи, участвовали А.А.Фокин, А.Е.Новодворский, А.В.Михалев, а также В.А.Смирнов, обеспечивший теоретико-логическую поддержку разработок.
Подобного рода проекты активно развиваются сейчас в различных научных центрах. Но описываемая здесь система обладает той особенностью, что она рассчитана на работу не с одной какой-либо логической системой, а с довольно широким их классом. Для этого используется специальный язык описания логических систем. И как только некоторая логическая система описана в терминах этого языка, она поддерживается программой.
Описываемая здесь система реализована для IBM PC совместимых компьютеров. Разработка осуществлена при содействии Института Логики, Когнитологии и Развития Личности. В ней, кроме автора настоящей статьи, участвовали А.А.Фокин, А.Е.Новодворский, А.В.Михалев, а также В.А.Смирнов, обеспечивший теоретико-логическую поддержку разработок.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Smirnov A. Система интерактивного доказательства теорем. // Logicheskie Issledovaniya / Logical Investigations. 1993. VOL. 2. C. 90-104.
Issue
Section
Papers
References
Смирнов В. Л. Формальный вывод и логические исчисления//М., 1972.
Логика и компьютер. Моделирование рассуждений и проверка правильности программ //М.,1990
Suppes Р. Takahashi S. An interactive calculus Theorem-рrover for continuity Properties. //J. Symbolic Computation 7.1989
Suppes P. Three Current Tutoring Systems and Future Needs / / Stanford.CA 1991.
Harper R., Honsell F., Plotkin G.. A framework on defining logics. In Proc. of the 2nd Annual Logic in Computer Sc. Conf., Ithaca// NY. June 1987.
Sawamura, Minami,Ohashi. Proof methods based on Sheet of Thought in EUODHILOS, //Fujitsu lab. Research Report. 1992.
Логика и компьютер. Моделирование рассуждений и проверка правильности программ //М.,1990
Suppes Р. Takahashi S. An interactive calculus Theorem-рrover for continuity Properties. //J. Symbolic Computation 7.1989
Suppes P. Three Current Tutoring Systems and Future Needs / / Stanford.CA 1991.
Harper R., Honsell F., Plotkin G.. A framework on defining logics. In Proc. of the 2nd Annual Logic in Computer Sc. Conf., Ithaca// NY. June 1987.
Sawamura, Minami,Ohashi. Proof methods based on Sheet of Thought in EUODHILOS, //Fujitsu lab. Research Report. 1992.