This chapter basically deals with Resolution based theorem proving, a more general version of reasoning than the "if A then B" type rules you find in PROLOG.

The chapter uses a notation from a public domain Resolution based theorem proving program called Otter from Argonne National Laboratories. I have tried it a little and it is fairly nice. They have C code, a 32-bit DOS binary, a Macintosh version, user manuals in various formats and some sample problems. This is available by http and by ftp.

A better source of sample problems is the Thousands of Problems for Theorem Provers collection by Geoff Sutcliffe and Christian Suttner. This collection is rather large, a gzipped file of 1M which, when gunzipped comes to 18M. In all likelihood the only problems you will want are the ones in the puzzles directory. This package is available from the University of Munich by ftp and by http or from James Cook University, Australia, by ftp and by http.

This section notes that there is a notation for predicate calculus that involves using the symbols, `implies', `is equivalent to', `for all' and `there exists' yet given statements in this notation these relations can all be eliminated to give a form called clausal form. Of course its quite easy to just write statements in clausal form in the first place.

This section gives a number of rules (binary resolution, UR-resolution, and hyperresolution) for deriving new, correct statements from existing statements.

Just blindly using the possible rules to solve a problem is not a good way to quickly find an answer. This section gives several heuristics that can speed the search (proof by contradiction, set of support, weighting and PROLOG's strategy). These help, but there is a lot left to be desired.

This contains a sample problem and its translation from English into clauses, then it is submitted to Otter for solution. This Otter program is in a PROLOG Programs Package.

PC theorem proving is useful for some special applications however some researchers think it is not particularly realistic in that it does not seem to be the way people operate and there are other theories that have been proposed to explain human reasoning. Of course believers in this formal logic approach like to think that the methods in this chapter are realistic or if they believe they are different from the way people work these researchers may say that formal logic methods may ultimately turn out to be be as good as or better than the human method.

I think what with the great amount of faulty reasoning going on today this topic ought to be required in every high school. On the other hand it is also an absolutely wonderful example of what is not working and will never work with respect to getting programs to duplicate human level capabilities. The statements you cook up to solve problems are designed to work in a very specific, very limited, idealized situation. It takes quite a lot intelligence on the part of the person writing the rules to do this. But after that, grinding away (as a program does) does not constitute intelligence. The program has no idea what it is dealing with, (people, cats, kangaroos, etc.) and it cannot fill in gaps or correct mistakes when the human programmer makes a mistake.

Real human logic is not discrete, it is analog and conclusions come with a confidence factor. For an example of how continuous valued logic can be formalized see "Beyond Associative Memories: Logics and Variables in Connectionist Models", by Ron Sun, from the Ohio State Neuroprose Archive. (The book only mentions this in one VERY short paragraph.)

There is just the merest mention of the work of Johnson-Laird and Byrne whose research on people indicate that people reason by constructing models of the situation and looking for counter-examples. I've never had time to read more than a little of their book, Deduction yet it seems to fit in rather well with my bias toward image processing. In a previous work called Mental Models Philip Johnson-Laird proposed the idea of mental models based on his research. In the introduction to Deduction they write that "Mental Models was well-received by cognitive scientists. The exception was the reaction of ardent advocates of rule theories - those who believe that reasoning depends on formal rules of inference". For a short article on research in human reasoning see "Roots of Reason" by Bruce Bower in Science News, volume 145, number 5, pp 72-75, January 29, 1994.

Let me add the following example of human reasoning. Answer this question: can you fit an elephant into your car, a regular full-size living adult elephant? You will quickly answer no. How did you solve this? I suggest you conjured up an image of an elephant alongside your car and quickly realized it would not fit. Now if I asked you to EXPLAIN the logic involved in the decision you could go forward and write lovely little predicate calculus clauses that contain the facts and rules involved and you could go ahead and prove that the elephant will not fit. (Doing this in predicate calculus is a bit of a nasty problem since you need to supplement predicate calculus with the idea of numbers and that one number can be greater than or less than another number.) The formal explanation comes after you reached the conclusion by processing images. Can anyone defend the idea that you reached your conclusion by using symbolic facts and rules rather than by processing images? And if you can't defend symbol processing in this case how can anyone claim that symbol processing is how human beings actually reason? If there are any good answers I will be happy to publish them here!!!