A SELF-DESCRIBING AXIOMATIC SYSTEM AS A SUGGESTED BASIS FOR A CLASS OF ADAPTIVE THEOREM PROVING MACHINES.

Abstract

An explicitly self-describing axiomatic system is presented whose set of rules of inference continually increases in size as new theorems are proved. A proof of consistency relative to formal arithmetic is outlined. Modified LISP programs are the function constants of the system. A class of possible adaptive theorem proving machines is outlined. Such machines construct proofs by successively refining proof 'outlines' which employ heuristics. New heuristics are generated by the same mechanism used to generate rules of inference and theorems. In the notation of the axiomatic system, a heuristic or a rule of inference is itself a well formed formula. (Author)

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1969
Accession Number
AD0686510

Entities

People

  • Thomas H. Westerdale

Organizations

  • University of Michigan

Tags

DTIC Thesaurus Topics

  • Arithmetic
  • Consistency
  • Material Separation Processes
  • Notation
  • Refining

Readers

  • Calculus or Mathematical Analysis
  • Distributed Systems and Data Platform Development
  • Parallel and Distributed Computing.

Technology Areas

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