
Accession Number : AD0686510
Title : A SELFDESCRIBING 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 selfdescribing 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