A SELF-DESCRIBING AXIOMATIC SYSTEM AS A SUGGESTED BASIS FOR A CLASS OF ADAPTIVE THEOREM PROVING MACHINES.
MICHIGAN UNIV ANN ARBOR LOGIC OF COMPUTERS GROUP
Pagination or Media Count:
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
- Theoretical Mathematics
- Computer Programming and Software