The book "Automated Theorem Proving: Theory and Practice" by Prof. Monty Newborn arrived a couple of days ago, and I had a quick flip through it yesterday. I'm most interested in the resolution theorem prover, THEO, which the book fully describes. The source code is included on the accompanying CD.
So I got to thinking: automated theorem provers (ATPs) are really fascinating. Insofar as we know how to theorise about intelligence, they're half of the answer. (The other half is creativity* - think Myers-Briggs NT, where N is creativity and T is logical inference).
But what could you do with a theorem-prover?
My first thought was some kind of virtual persona. There are already virtual pets, like Felix the cat, which wander around your desktop. Perhaps an ATP-powered virtual pet could be a winner, a kind of less-idiotic chatbot.
ATPs are optimised to build deep proof trees from rather sparse axiom sets. But the kind of commonplace reasoning which underlies chat is the opposite - shallow inference based on a large amount of shared contextual experience. "In the knowledge is the power" as the Expert Systems people used to say.
It's an endless task of knowledge engineering to try to manually enter 'commonsense knowledge' - that way lies madness and the Cyc project. Instead, one should either let other people do it for you, or create an embodied AI system (aka a baby) which can learn all this stuff by itself, through normal social interaction. That's a dream which has been around for a while.
So we come to the Internet. An agent on the web, with appropriate interfaces, can be 'trained' by all the people who care to interact with it. Just (non-trivially) filter out the dodgy stuff.
So we get to three key questions.
1. How good does a system like this have to be to get people to want to engage with it? Better, clearly, than a pattern-shuffling chatbot, but maybe not that much better. Most people seem to desire above all a good listener who seems to stay engaged.
2. How much effort would it be to program? I have no spare cash for hiring servers, so the system should run on the user's machine. Java applets is the model, but THEO is in C, and I prefer to write all this stuff in Lisp. We also need somehow to build a central knowledge-base.
3. How do we make money out of it? Charging for use is out of the question. There are two routes I can see: the first is to do some content analysis of the conversations and link up with Google adwords (as proposed for Gmail); the second is to sell the system to a cyberpet maker such as the 'Fur Real' people who sold us our cat, to spice up their interaction model.
+++
* Creativity is not as mysterious as it looks. It seems to come down to the ability to see structural similarities between different kinds of knowledge (similar to metaphor) and then to map what is known in one domain into another through a kind of generate-and-test process. This kind of formula-processing uses many of the basic procedures, such as unification, found in ATP.
NOTE: This is all whimsical stuff BTW. If you look at the current state-of-the-art in all this, the level of sophistication is frightening. Like computer games, it's gone well past amateur stage.
