Interactive theorem retrieval and generation
Paul S. Jensen · 1968
When developing or extending a technique for solving some mathematical problem, one normally spends a considerable amount of time recalling and searching the literature for information and theorems applicable to the subject. Because of the way that information on a subject tends to be sprinkled throughout the literature, the process of gathering the known facts on the subject is often inefficient and time consuming.