🚀 go-pugleaf

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.