On Explicit Reflection in Theorem Proving and Formal Verification
CORNELL UNIV ITHACA NY CENTER FOR FOUNDATIONS OF INTELLIGENT SYSTEMS
Pagination or Media Count:
The basic properties of soundness, extensibility, and stability required from a verification system V taken in full yield the necessity of having a reflection rule in every such V. However, the reflection rule based on the Godel provability predicate implicit provability predicate leads to a reflection tower of theories which cannot be formally verified. The paper introduces an explicit reflection mechanism which can be verified inside the system. This circumvents the reflection tower and provides a strict justification for the verification process. On the practical side, the paper gives specific recommendations concerning the verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.
- Theoretical Mathematics
- Computer Programming and Software