# Accession Number:

## AD0686510

# Title:

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

# Descriptive Note:

## Technical rept.,

# Corporate Author:

## MICHIGAN UNIV ANN ARBOR LOGIC OF COMPUTERS GROUP

# Personal Author(s):

# Report Date:

## 1969-03-01

# Pagination or Media Count:

## 266.0

# 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

# Descriptors:

# Subject Categories:

- Theoretical Mathematics
- Computer Programming and Software