NEWSLETTER

No. 59, June 2003

From the AAR President

Announcement of the 2003 Herbrand Award

Call for Nominations: CADE Trustees Election

Call for Submissions

Call for Contributions: QPQ Deductive Software Repository

Open Question

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.

(Secretary of AAR and CADE)

E-mail: mariapaola.bonacina@univr.it

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

Nominations can be made by any AAR member, either by e-mail or in person at the CADE 2003 business meeting. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be or be willing to become AAR members. For further details please see the CADE Inc. bylaws at the Web site.

The board of trustees currently includes (in alphabetical order):

Franz Baader, CADE 2003 program chair, Germany

David Basin, IJCAR 2004 program co-chair, Switzerland

Maria Paola Bonacina, Secretary, Italy

Gilles Dowek, elected 9/2001, France

Ulrich Furbach, President, elected 8/1997 and 10/2000, Germany

Harald Ganzinger, former program chair, elected 10/1999 and 10/2002, Germany

John R. Harrison, elected 9/2001, U.S.A.

Michael Kohlhase, elected 10/2000, U.S.A.

David McAllester, former program chair, elected 10/2000, U.S.A.

Neil V. Murray, Treasurer, U.S.A.

Frank Pfenning, Vice-President, elected 10/1998 and 9/2001, U.S.A.

Andrei Voronkov, former program chair, elected 10/2002, U.K.

Toby Walsh, elected 10/2002, Ireland

The terms of Ulrich Furbach, Michael Kohlhase and David McAllester expire after CADE 2003, because CADE Trustees are elected for three years. The term of office of Franz Baader also expires with CADE 2003, but his position is taken by David Basin as IJCAR 2004 program co-chair. Thus, there are three trustees to elect (the IJCAR 2004 program co-chairs are David Basin and Michael Rusinowitch; the CADE trustees offered them to serve on the board, and they agreed that David will).

Among the outgoing trustees, Michael Kohlhase and David McAllester are eligible to be nominated for a second term, and Franz Baader is eligible to be nominated for a first term as elected trustee; Ulrich Furbach is not eligible because one cannot be elected for three consecutive terms.

E-mail nominations are to be sent to
`CADE-board@sci.univr.it`
before the end of CADE (August 2, 2003).

Posters are sought in all areas of logic programming:

- Theory (semantic foundations, formalisms, non-monotonic reasoning, knowledge representation, inductive logic programming)
- Language issues (constraints, concurrency, objects, coordination, higher order, types, modes, programming techniques)
- Implementation (compilation, memory management, virtual machines, parallelism)
- Environments (program analysis, program transformation, validation and verification, debugging)
- Applications (deductive databases, software engineering, natural language, Web tools, Internet agents, artificial intelligence, molecular biology)

Posters provide an excellent forum for presenting late-breaking or speculative work in an interactive and informal setting. Submission details for papers and posters can be found on the conference Web page. Submission deadline is June 28, 2003.

Two kinds of submission are invited:

- Research papers on inference methods in computational semantics as well as their applications (10 pages).
- System descriptions (6 pages) focusing on actual implementations and explaining system architecture issues and specific implementation techniques. The systems described will be demonstrated at ICoS-4.

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.

For further information, see the Web site.

*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.

Submissions of deductive software systems, components, and applications are welcome; the submissions must be relevant to automated deduction. Examples include matching and unification procedures, rewrite engines, BDD packages, SAT solvers, model checking tools, decision procedures, induction analyzers, proof search engines, term indexing libraries, benchmark suites, formalization libraries, editors and user interface tools, language processors, program synthesis and transformation systems, and innovative applications. Authors may choose to have their submissions refereed for design, functionality, efficiency, and documentation. Accepted submissions will be published through the QPQ Web site. For more information regarding membership in the repository and submission and editorial guidelines, visit the QPQ Web site. The QPQ Manifesto can be read at the Web site.

A workshop on the QPQ deductive software repository will be held on July 28, 2003, as part of the CADE-19 conference at Miami, Florida.

E-mail wos@mcs.anl.gov

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.

Gail Pieper

June 2003