Computational Uses of the Manipulation of Formal Proofs

Abstract

This thesis concerns computational uses of the additional information contained in proofs, and efficient methods for the representation and transformation of proofs. An extended lambda-calculus is presented which allows compact expression of the computationally significant part of the information contained in proofs. Terms of the calculus preserve dependency data, but can be efficiently executed by an interpreter of the kind used for lambda-calculus based languages such as LISP. The calculus has been implemented on the Stanford Artificial Intelligence Laboratory PDP-10 computer. Results of experiments on the use of pruning transformations in the specialization of a bin-packing algorithm are reported.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1980
Accession Number
ADA091180

Entities

People

  • Christopher Alan Goad

Organizations

  • Stanford University

Tags

Communities of Interest

  • Biomedical
  • C4I
  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Computational Complexity
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Construction
  • Language
  • Law
  • Mathematical Analysis
  • Mathematics
  • Programming Languages
  • Recursive Functions
  • Simplex Method
  • Standards

Fields of Study

  • Computer science

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.
  • Neural Network Machine Learning.

Technology Areas

  • AI & ML
  • AI & ML - Neural Networks