1999 | OriginalPaper | Chapter
On Explicit Reflection in Theorem Proving and Formal Verification
Author : Sergei N. Artemov
Published in: Automated Deduction — CADE-16
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.