ok@goanna.cs.rmit.OZ.AU (Richard O'keefe) (05/03/90)
I got a very pleasant surprise yesterday: The Logical Basis for Computer Programming Volume 2: Deductive Systems Zohar Manna & Richard Waldinger Addisson-Wesley 0-201-18261-0 is out! My copy cost AUS$42.95, which given Australian markups probably means that you get it in your cornflakes in the US. The introductory paragraph of the Preface says Welcome to Volume II of "The Logical Basis for Computer Programming". In Volume I, we have given a general introduction to logic, emphasising theories of importance to computer science, such as strings, trees, lists, and sets. Our presentation was rigorous but informal: we described the theories by giving axioms but used ordinary commonsense reasoning in deriving valid sentences from these axioms. In Volume II, we are more formal: in place of our common sense, we present a "deductive tableau" system for proving the validity of sentnces. The deductive system we provide is "machine-oriented": it is suitable for implementation in an automatic or interactive computer theorem- proving program. Basically, the focus in the two volumes is logic _in use_ rather than the theory of logic. I presume that many of the people using Prolog do so because they are interested in the relationship between logic and programming; if that's you, you'll find these books a good read.