Efficient Representation and Validation of Logical Proofs

Abstract

This report describes a framework for representing and validating formal proofs in various axiomatic systems. The framework is based on the Edinburgh Logical Framework (LF) but is optimized for minimizing the size of proofs and the complexity of proof validation, by removing redundant representation components. Several variants of representation algorithms are presented with the resulting representations being a factor of 15 smaller than similar LF representations. The validation algorithm is a reconstruction algorithm that runs about 7 times faster than LF typechecking. We present a full proof of correctness of the reconstruction algorithm and hints for the efficient implementation using explicit substitutions. We conclude with a quantitative analysis of the algorithms.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1997
Accession Number
ADA332310

Entities

People

  • George C. Necula
  • Peter P Lee

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Autonomy
  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Arithmetic
  • Assembly Languages
  • Calculus
  • Computer Programming
  • Computer Science
  • Construction
  • Language
  • Network Protocols
  • Notation
  • Programming Languages
  • Redundancy
  • Redundant Components
  • Side Effects
  • Symbols
  • Validation

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Linguistics
  • Computational Modeling and Simulation