1. Embed a clean programming language into your logic.
This is so that the system can reason about the algorithms it uses.
See HOST for a sketch of the kind of logic you need for this.
2. Incorporate a Reflection Principle into your logic. So if we know an algorithm is reliable we can use it to solve a problem and use the result in a proof.
3. Code up a wide range of specific problem solving techniques
Most people learn methods out of books or off other people.
They don't work them out for themselves.
4. Use Axioms or other techniques to defer proof obligations Functionality first, assurance next. When the machine gets good, it can come back and do the proofs itself.
|Steps 1-4 enable problem solving using efficient algorithms within the context of a general proof based problem solving framework. It uses human coding ingenuity to get near optimal solutions in all those specific problem domains where techniques are known. Before the system can do this kind of thing for itself it must learn programming methods and theory. Coding up methods is the most efficient analogue to learning by rote. So we teach it programming the same way in the first instance.|
|5. Code up programming methods. There is an enormous amount of this to be done before the system has any chance of being intelligent. To get over the hump we have to make this pay as it goes, so this system has to be a productive software development envuronment long before it ever gets to be an artificial intelligence.||6. Eventually the system is able to code up its own efficient problem solving methods. And sometime after that it really gets to be intelligent, in this narrow logical domain: logic, mathematics, computer programming. Then, like us humans, it will sometimes be able to solve novel problems despite combinatorial explosion.|