Система интерактивного доказательства теорем.
Article Sidebar
Опубликован:
04.11.1993
Main Article Content
Аннотация
В настоящей статье списана система интерактивного поиска доказательства Deductio. Она позволяет строить доказательства, гарантируя их корректность. При этом пользователю доступны различные средства автоматизации.
Подобного рода проекты активно развиваются сейчас в различных научных центрах. Но описываемая здесь система обладает той особенностью, что она рассчитана на работу не с одной какой-либо логической системой, а с довольно широким их классом. Для этого используется специальный язык описания логических систем. И как только некоторая логическая система описана в терминах этого языка, она поддерживается программой.
Описываемая здесь система реализована для IBM PC совместимых компьютеров. Разработка осуществлена при содействии Института Логики, Когнитологии и Развития Личности. В ней, кроме автора настоящей статьи, участвовали А.А.Фокин, А.Е.Новодворский, А.В.Михалев, а также В.А.Смирнов, обеспечивший теоретико-логическую поддержку разработок.
Подобного рода проекты активно развиваются сейчас в различных научных центрах. Но описываемая здесь система обладает той особенностью, что она рассчитана на работу не с одной какой-либо логической системой, а с довольно широким их классом. Для этого используется специальный язык описания логических систем. И как только некоторая логическая система описана в терминах этого языка, она поддерживается программой.
Описываемая здесь система реализована для IBM PC совместимых компьютеров. Разработка осуществлена при содействии Института Логики, Когнитологии и Развития Личности. В ней, кроме автора настоящей статьи, участвовали А.А.Фокин, А.Е.Новодворский, А.В.Михалев, а также В.А.Смирнов, обеспечивший теоретико-логическую поддержку разработок.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Смирнов А. Система интерактивного доказательства теорем. // Логические исследования / Logical Investigations. 1993. Т. 2. C. 90-104.
Выпуск
Раздел
Статьи
Литература
Смирнов В. Л. Формальный вывод и логические исчисления//М., 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.