sjmz@hplb.CSNET (Stefek Zaba) (07/13/87)
In response to the points of Jim Hendler and John Nagle, about whether you can verify that your favourite planning system can be shown to be more general than the Standard Reference: At the risk of drawing the slings and arrows of people who sincerely believe Formalism to be the kiss of death to AI, I'd argue that there *are* better characterisations of the power of algorithms than a battery of test cases - or, in the case of the typical reported AI program, described in necessarily space-limited journals, a tiny number thereof. Such characterisations are in the form of more formal specs of the algorithm - descriptions of it which strip away implementation efficiency tricks, and typically use quantification and set operations to get at the gist of the algorithm. You can then *prove* the correctness of your algorithm *under given assumptions*, or "equivalently" derive conditions under which your algorithm produces correct results. Such proofs are usually (and, I believe, more usefully) "rigorous - but - informal"; that is a series of arguments with which your colleagues cannot find fault, rather than an immensely long and tortuous series of syntactic micro-steps which end up with a symbol string representing the desired condition. Often it's easier to give sufficient (i.e. stronger than necessary) conditions under which the algorithm works than a precise set of necessary-and-sufficient ones. *Always* it's harder (for mere mortals like me, anyway) than just producing code which works on some examples. An example of just such a judicuious use of formalism which I personally found inspiring is Tom Mitchell's PhD thesis covering the version space algorithm (Stanford 1978, allegedly available as STAN-CS-78-711). After presenting a discursive description of the technique in chapter 2, chapter 3 gives a formal treatment which introduces a minimum of new terminology, and gives a simple and *testable* condition under which the algorithm works: "A set of patterns P with associated matching predicate M is said to be an admissible pattern language if and only if every chain [totally ordered subset] of P has a maximum and a minimum element". Stefek Zaba, Hewlett-Packard Labs, Bristol, England. [Standard disclaimer concerning personal nature of views applies]