I hail the efforts of Mark Stickel in establishing an open source repository for deductive software. Having a variety of tools and libraries available will, I hope, encourage researchers to experiment with different systems and procedures, perhaps using the benchmark suites that are also provided. I strongly encourage AAR members to visit this new site.

I also encourage researchers to attack the open question in combinatory logic presented at the end of this newsletter. If you succeed in finding an answer, I would be most delighted to hear from you.

Peter B. Andrews will be awarded the Herbrand Award at CADE 2003 for his seminal contributions and pioneering research in type theory, mating-based theorem proving, automated deduction in higher-order logic, logic education, and many other contributions to the field of automated reasoning.

Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held next fall.

Submission deadline is June 30, 2003. Submission is by e-mail. Either Postscript or PDF files can be sent to icos4@aplog.org.

The workshop proceedings will be distributed at the conference; plans are also under way to publish a selection of accepted papers as a special journal issue.

An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edition by Peter B. Andrews

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's unifying principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's theorem, unification, duality, interpolation, and definability.

The last three chapters of the book provide an introduction to type theory (higher-order logic). The author shows how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models, which is important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's paradox about countable models of set theory.

Some of the numerous exercises require giving formal proofs. A computer program called ETPS, available from the Web, facilitates doing and checking such exercises.

This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.

Kluwer Academic Publishers, Dordrecht
Hardbound, ISBN 1-4020-0763-9
408 pages; EUR 88.00 / USD 81.00 / GBP 55.00

QPQ is an open source repository for deductive software components. It represents a community effort for publishing, preserving, and maintaining high-quality deductive software in source code form. Dr. Mark Stickel is the editor-in-chief of QPQ.

In combinatory logic, various fragments are studied in terms of specific combinators. A particularly difficult problem in this area has focused on the basis consisting of S and K alone, which provides a basis for all of combinatory logic. Sxyz = xz(yz) and Kxy = x. (By convention, all expressions are left associated unless otherwise indicated.) Of interest is whether the strong fixed point property holds for the fragment whose basis consists of S and K alone. To be such a fixed point combinator F, it must be that Fy = y(Fy) for all y.

You are presented specifically with three challenges:

1. Prove that such an F exists in terms of S and K.

2. Using an automated reasoning program and without guidance, find such a combinator.

3. John Tromp found a combinator of length 12. Using an automated reasoning program, find a combinator of length 12 or shorter. Even better, prove that no shorter one exists, or find a shorter one.