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) : Westerdale,Thomas H.

Report Date : MAR 1969

Pagination or Media Count : 266

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 :   (*MATHEMATICAL LOGIC, COMPUTER PROGRAMMING), PROBLEM SOLVING, FUNCTIONS(MATHEMATICS), THESES, COMPUTER LOGIC, ADAPTIVE SYSTEMS

Subject Categories : Theoretical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE