Accession Number:

ADA364427

Title:

On Explicit Reflection in Theorem Proving and Formal Verification

Descriptive Note:

Technical rept.

Corporate Author:

CORNELL UNIV ITHACA NY CENTER FOR FOUNDATIONS OF INTELLIGENT SYSTEMS

Personal Author(s):

Report Date:

1998-12-01

Pagination or Media Count:

19.0

Abstract:

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.

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE