Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!uunet!husc6!ut-sally!brian
From: brian@ut-sally.UUCP (Brian H. Powell)
Newsgroups: comp.ai
Subject: Re: The Success of AI
Message-ID: <9320@ut-sally.UUCP>
Date: Mon, 19-Oct-87 13:47:45 EDT
Article-I.D.: ut-sally.9320
Posted: Mon Oct 19 13:47:45 1987
Date-Received: Tue, 20-Oct-87 06:35:45 EDT
References: <228@snark.UUCP>
Organization: U. Texas CS Dept., Austin, Texas
Lines: 47

In article <228@snark.UUCP>, eric@snark.UUCP (Eric S. Raymond) writes:
> Doug Lenat's Amateur Mathematician program was a theorem prover equipped with
> a bunch of heuristics about what is 'mathematically interesting',
> [...]
> 
> After n hours of chugging through a lot of nontrivial but already-known
> mathematics, it 'conjectured' and then proved a bunch of new results on the
> [...]

     I feel compelled to challenge this, but not necessarily the rest of your
article.
     AM wasn't a theorem prover.  From the July, 1976 dissertation:

7.2.2 Current Limitations

[...]
AM has no notion of proof, proof techniques, formal validity, heuristics for
finding counterexamples, etc.  Thus it never really establishes any conjecture
formally.
			---end of excerpt---

     The dissertation goes on to briefly suggest ways of adding this
capability, but as I understand it, no one ever has.  Lenat himself, as I
recall, thought it was more interesting to do more work towards heuristics
than proving.  EURISKO was the result of that.  (i.e., you might get more
power if you could spend part of your time conjecturing heuristics in addition
to conjecturing about particular problems.)
     AM is a neat program, but by many views it's overrated.  It's great that
it conjectures all these neat theorems, but my impression is that it does
quite a bit of floundering to find them.  I think it also spends a lot of time
floundering without finding anything useful, also.  (A program run isn't
guaranteed to think of something clever.)  Finally, it's not clear that the
program is really intelligent enough to realize that it's just conjectured
something intelligent.  (I would bet that there are a lot of things AM has
considered uninteresting that humans consider interesting, and vice-versa.)
     A human can monitor AM and modify the priority of certain tasks if the
human feels AM is studying the wrong thing.  A human is practically required
for this purpose if AM is to do something especially clever.  This turns AM
more into a search tool than an autonomous program, and I don't think a tool
is what Lenat had in mind.
     If you read the summaries of AM, you think it's powerful.  Once you read
the entire dissertation, you realize it's not quite as great a program as you
had thought, but you still think it's good research.

Brian H. Powell
		UUCP:	...!uunet!ut-sally!brian
		ARPA:	brian@sally.UTEXAS.EDU