Automated Reasoning and Its Applications: Essays in Honor of Larry Wos

Rating:
Summary: Of historical interest
Review: This book overviews the status of research in automated reasoning as it stood in 1997, but with emphasis on the work of Larry Wos, and one year after the announcement of the proof of the Robbins conjecture by the EQP reasoning machine. The book is still worth perusing, even though it is seven years out of date, and there has been a considerable amount of work done in the field of automated reasoning since 1997. Much of this work has involved dealing with the informal nature of mathematical proofs as they are currently done in most of the mathematical research literature, and thus involves research both in natural language processing and in automated reasoning. The applications of automated reasoning have to this date involved deductive databases and formal checking of computer systems and circuit designs. The field of automated reasoning is of course of great importance to those involved in the construction of intelligent machines. Throughout this book proof systems such as OTTER (for Organized Techniques for Theorem proving and Effective Research) are referred to quite frequently. OTTER is now one of the most popular systems for the exploration of automated reasoning, and is publicly available. Due to constraints of space, only selected articles of the book will be reviewed here.

The notion of linked resolution is discussed in the second article of the book, which is a strategy used to deal with "uninteresting" clauses in resolution-based provers. Linked resolution will perform proof steps until an "interesting" clause is derived, which it will retain and then eliminate the intermediate results. It does this by identifying a collection of clauses called `linking clauses', which are used as a nucleus only in certain steps, like a hyperresolution clash. The author of the article proves a completeness theorem for predicate logic without equality that incorporates linked resolution, and considers this result a generalization of the completeness of hyperresolution. He emphasizes though that adding equality and paramodulation will eliminate the completeness result.

The third article in the book discusses Isabelle, which is a theorem prover that is based upon resolution, and searches for proofs using a tableau approach. It is, according to the author of the article, a `generic' reasoner, in that it can work in a variety of domains without reducing them to first-order logic. Isabelle is also `interactive' meaning that its user can direct each step of the proof. Interactive provers are to be distinguished from the `resolution' systems such as OTTER, but Isabelle is also based upon a form of resolution, and therefore represents a "synthesis" between the these two traditions in automated reasoning. The author thus describes Isabelle as an interactive prover based on the typed lambda-calculus, and uses as its primary inference rule a generalization of Horn clause resolution. The author outlines in detail the tableau approach, and uses Isabelle to prove classical results in set theory and first-order logic and proves the Church-Rosser theorem for combinators. When reading the article one sees immediately the connection of Isabelle with higher-order logic, it being a `meta-logic' that supports `object-logics' (the meta-logic supporting connectives, implication, and equality), making use of functions called `tacticals' that operate on proof states called `tactics', with concepts from logic programming used to support automation on the tactics and tacticals.

The fifth article in the book, written by William McCune, who is responsible for the use of EQP and its consequent proof of the Robbins conjecture, is an overview of how to evaluate the `paramodulation' strategies using EQP. A test collection of 33 equational theorems is used for this evaluation, and the performance of OTTER and EQP are compared on this collection. The proof of the Robbins conjecture, because of the timing in publishing this book, is not included, as it was solved by EQP, as the author indicates, after this article was finished. The author though describes in some detail the Robbins algebra, and in a footnote briefly discusses how the Robbins conjecture was proven.

The most interesting of the articles in the book is the last one, which concerns what the author of article calls "metalevel reasoning", and its role in controlling automated reasoning programs. He defines metalevel reasoning as being the reasoning with facts and knowledge beyond the symbols of the formula given to the basic reasoning system. This notion encapsulates perfectly the process by which human mathematicians have generated proofs for the last few centuries. Unlike the case of the formal and automated reasoning systems that have been developed over the last five decades, human mathematicians use ordinary language and extraneous knowledge that is typically outside of the scope or domain of the problem they are analyzing. Automated reasoning systems developed up until now do not do this, says the author, but instead manipulate the symbols of formulas according to a collection of inference rules. A reasoning system that incorporates metareasoning would be an enormous benefit argues the author, and could provide the "proving" expertise that is now introduced by fiat by the developer or user of the reasoning system. He gives a few examples of metalevel reasoning, and gives an overview of just how a reasoning system that incorporated it would behave. The author also discusses how metalevel control has been studied in the context of general research in artificial intelligence. The research that he describes in this article is now occupying the time of many researchers in automated reasoning and automated theorem proving, and if it comes to fruition will represent a major advance in machine intelligence. For a machine to be able to generate and prove theorems in the manner that human mathematicians are able to, would be an example of machine creativity and has enormous potential in real-world applications such as bioinformatics, automated scientific discovery, network management, and financial engineering. It is for this reason that this reviewer regards this type of research into automated reasoning as being the most important of all activities to date.