The Nearly Ultimate Pearl
No Access Until
Permanent Link(s)
Collections
Other Titles
Author(s)
Abstract
The PRL ("pearl") system is an environment providing computer assistance in the construction of formal proofs and programs in a particular formal theory, called the object theory. Certain proofs can in fact be considered as programs. The system embodies knowledge about programs in the form of rules of inference and in the form of facts stored in its library. Ultimately PRL may be regarded as an intelligent system for formal constructive problem solving in a large domain of mathematics. The PRL system is evolving in stages. Since our report "The Definition of Micro-PRL" in October 1981, we have had the experience of designing, building and using a complete core version of the system (called