There have been (and continue to be) many approaches to this, in fact the term Good old fashioned AI basically refers to this. It is very interesting that significant progress has not been made with this approach. This has led to greater use of statistical techniques, such as support vector machines or Bayesian networks. A basic difficulty with any approach to AI is that many techniques merely change the problem of learning, generalisation and problem solving into another form rather than solving it. E.g. Formal methods for software development move the problem from that of programming to that of formal specification. It’s not clear that creating the specifications is any less error prone than the creation of the original program.
On the other hand there are enormous benefits to turning any knowledge into a form that a computer can manipulate. There has been some progress in doing this for mathematics. It is possibly one of the most depressing consequences of Godel’s theorem that there has not been more work in this area. Writing proofs informally on paper doesn’t get around Godel’s theorem, it just makes the work harder to validate.
It’s also a good challenge for those who feel that AI is just a matter of correctly applying Bayes theorem, as it is not clear how it could be applied to solve this problem.
There have been (and continue to be) many approaches to this, in fact the term Good old fashioned AI basically refers to this. It is very interesting that significant progress has not been made with this approach. This has led to greater use of statistical techniques, such as support vector machines or Bayesian networks. A basic difficulty with any approach to AI is that many techniques merely change the problem of learning, generalisation and problem solving into another form rather than solving it. E.g. Formal methods for software development move the problem from that of programming to that of formal specification. It’s not clear that creating the specifications is any less error prone than the creation of the original program.
On the other hand there are enormous benefits to turning any knowledge into a form that a computer can manipulate. There has been some progress in doing this for mathematics. It is possibly one of the most depressing consequences of Godel’s theorem that there has not been more work in this area. Writing proofs informally on paper doesn’t get around Godel’s theorem, it just makes the work harder to validate.
It’s also a good challenge for those who feel that AI is just a matter of correctly applying Bayes theorem, as it is not clear how it could be applied to solve this problem.