|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
On explicit reflection in theorem proving and formal verificationстатья
Информация о цитировании статьи получена из
Scopus
Дата последнего поиска статьи во внешних источниках: 26 августа 2016 г.
- Автор: Artemov Sergei
- Сборник: Automated Deduction – CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings
- Серия: Lecture Notes in Computer Science
- Том: 1632
- Год издания: 1999
- Место издания: Springer
- Первая страница: 267
- Последняя страница: 281
- DOI: 10.1007/3-540-48660-7_23
- Аннотация: We show that the stability requirement for a verication system yields the necessity of some sort of a reflection mechanism. However, the traditional reflection rule based on the Göodel implicit provability predicate leads to a “reflection tower” of theories which cannot be formally veried. We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verication system. The paper also introduces an explicit reflection mechanism which can be veri ed internally. This circumvents the reflection tower and provides a theoretical justication for the verication process. On the practical side, the paper gives specic recommendations concerning verication of inference rules and building a veriable reflection mechanism for a theorem proving system.
- Добавил в систему: Золин Евгений Евгеньевич