On Explicit Reflection in Theorem Proving and Formal Verification

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1998
Accession Number
ADA364427

Entities

People

  • Sergei N. Artemov

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Artificial Intelligence
  • Computer Science
  • Consistency
  • Information Operations
  • Intelligent Systems
  • Language
  • Logic
  • Mathematics
  • Military Research
  • Reflection
  • Set Theory
  • Standards
  • Theorems
  • Universities
  • Verification

Readers

  • Computational Linguistics
  • Electromagnetic Wave Scattering and Antenna Radiation Engineering
  • Software Engineering.

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms
  • AI & ML - Machine Translation