NEWSLETTER

No. 56, September 2002

**Contents**

From the AAR President

Second IJCAR to Be Held in 2004

Announcement of the 2002 Herbrand Award

News from the Secretary

Announcement of CADE Elections

Thesis Abstracts

Call for Papers

Logic and Automated Reasoning Summer School

Book Announcement

Special Issues

Automated Reasoning to be held in 2004

(mariapaola.bonacina@univr.it)

After several years of gradual fragmentation of the Automated Reasoning community into various conferences and workshops, the CADE/AAR, FTP and TABLEAUX communities decided to have a joint conference, the International Joint Conference on Automated Reasoning (IJCAR), held in Siena (Italy), June 18-23, 2001.

IJCAR 2001 was regarded as a clear success
and the IJCAR Business Meeting in Siena voted overwhelmingly
to have a second IJCAR. In the fall of 2001,
the CADE Inc. Board of Trustees, the FTP Steering
Committee and the TABLEAUX Steering Committee
agreed to have the **Second International Joint
Conference on Automated Reasoning in 2004**,
welcoming also the Workshop on Frontiers of Combining Systems (FroCoS).
In the summer of 2002, the Calculemus Symposium,
which had already co-located with IJCAR 2001,
also joined IJCAR proper.

The CADE board of trustees and the steering committees of Calculemus, FroCoS, FTP, TABLEAUX, respectively, agree to the following:

**Basic Statement:**
CADE, Calculemus, FroCoS, FTP and TABLEAUX agree to have IJCAR together
and IJCAR will replace these events in 2004.

**Conference Chair and Location:** Toby Walsh, University College Cork,
Cork, Ireland.

**Program Committee:**
IJCAR 2001 had three program co-chairs, designated by its constituent meetings,
respectively.
In order to foster integration, IJCAR 2004 will have two program co-chairs,
selected as follows:
the CADE board of trustees and the steering committees of
Calculemus, FroCoS, FTP, TABLEAUX, respectively,
will make up to two nominations each.
The IJCAR steering committee will propose two names out of the slate of
all nominees from the constituent meetings,
and ask the latter to accept them or suggest motivated changes,
till a reasonable consensus is reached in reasonable time.
This procedure was also presented at the
Business Meetings of CADE and Tableaux during FLoC 2002 and met no objection.

**Program:**
Similar to 2001, it is expected that the
program co-chairs will choose a balanced program
committee with significant representation from all
participating communities, and the scope of the
joint conference will be at least the union of the
scopes of the constituent meetings.
IJCAR will invite submission related to all aspects of automated
reasoning, including foundations, implementations, and applications.

**Proceedings:**
As in 2001 there will be one common set of proceedings and the editors will
be the two program co-chairs.

**Other officers:**
The program co-chairs will appoint
workshop chair, tutorial chair and publicity chair,
possibly in consultation with the steering or program committee.
The conference chair may appoint a treasurer,
possibly in consultation with the steering committee,
and a local arrangements chair or committee at his discretion.

**IJCAR Steering Committee:**
IJCAR 2001 had a steering committee formed of
the conference chair, the three program co-chairs and
up to two representatives per constituent meeting.
In order to accomodate the new entries while
keeping the committee's size reasonable,
the IJCAR 2004 steering committee will include the following:
the IJCAR conference chair,
the previous IJCAR conference chair (for continuity),
the two IJCAR program co-chairs,
and one representative per constituent meeting.

At present, this results in the following list:

Alessandro Armando (FroCoS), Christoph Benzmueller (Calculemus), Maria Paola Bonacina (FTP), Ulrich Furbach (CADE), Reiner Haehnle (Tableaux), Fabio Massacci (former conference chair), Toby Walsh (conference chair), with the two program co-chairs yet to be determined, and Maria Paola Bonacina as coordinator.

**Finances:**
CADE Inc. will back financially IJCAR 2004 at the same conditions
of 2001: in case of loss, CADE Inc. bears the loss;
in case of profit, the revenue goes into the CADE Inc. account,
with 25% earmarked to support future CADEs, and 75% earmarked
to support future IJCARs.

Comments and suggestions from all members of the AAR community are very welcome and will be carefully listened to.

**CADE Trustees (CADE-board@sci.univr.it):**
Franz Baader (CADE 2003 program chair),
Maria Paola Bonacina (Secretary), Gilles Dowek, Ulrich Furbach (President),
Harald Ganzinger (outgoing), John R. Harrison, Michael Kohlhase, David McAllester,
Neil V. Murray (Treasurer), Frank Pfenning (Vice-President),
David A. Plaisted (outgoing), Andrei Voronkov (CADE 2002 program chair: outgoing).

**Calculemus Trustees:**
Michael Beeson, Wolfgang Windsteiger, James Davenport,
Alessandro Armando, Steve Linton, Roberto Sebastiani,
Volker Sorge, Olga Caprotti, Therese Hardin, Renaud Rioboo,
Andrzei Trybulec, Silvio Ranise.

**FroCoS Steering Committee (frocos-sc@mrg.dist.unige.it):**
Alessandro Armando, Franz Baader, Christoph Ringeissen, Klaus U. Schulz.

**FTP Steering Committee (ftp-sc@logic.at):**
Alessandro Armando, Peter Baumgartner, Maria Paola Bonacina (President),
Ricardo Caferra, Domenico Cantone, David Crocker, Ingo Dahn, Bernhard Gramlich,
Reiner Haehnle, Alexander Leitsch, Paliath Narendran, Christoph Weidenbach.

**TABLEAUX Steering Committee (reiner@cs.chalmers.se):**
Marcello D'Agostino, Uwe Egly, Chris Fermüller, Melvin Fitting, Ulrich Furbach,
Didier Galmiche, Rajeev Gore, Reiner Haehnle (President), Fabio Massacci,
Peter H. Schmitt (Vice-President).

(Secretary of AAR and CADE)

An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people are currently serving as Trustees of CADE Inc.:

Franz Baader (CADE 2003 Program Chair)

Maria Paola Bonacina (Secretary)

Gilles Dowek (elected 9/2001)

Ulrich Furbach, President (elected 8/1997 and re-elected 10/2000)

Harald Ganzinger (past Program Chair, elected 10/1999: term expired)

John R. Harrison (elected 9/2001)

Michael Kohlhase (elected 10/2000)

David McAllester (past Program Chair, elected 10/2000)

Neil V. Murray (Treasurer)

Frank Pfenning, Vice-President (elected 10/1998 and re-elected 9/2001)

David A. Plaisted (elected 10/1999: term expired)

Andrei Voronkov (CADE 2002 Program Chair: term expired)

The terms of office of Harald Ganzinger and David Plaisted are expiring, because CADE trustees are elected to serve for three years, as well as that of Andrei Voronkov. The position of Andrei Voronkov is replaced by Franz Baader, as CADE 2003 Program Chair. Nonetheless, there are three positions to fill, because CADE Inc. is implementing the amendment to its bylaws, approved by the membership in the summer of 2000, that requires to increase the number of trustees from nine to twelve, by electing three trustees instead of two for three elections. The first two elections with an additional slot were held in 2000 and 2001, and this is the third such election (see AAR Newsletter No. 48, August 2000).

The following candidates were nominated:

and provided the following statements.

On the other side, CADE needs to remain well embedded into its neighboring disciplines both on the theoretical side (logic in computer science, term rewriting) and on the practical side (verification, knowledge representation, logic programming, computer algebra). As CADE trustee I would continue to pursue the tasks implied by this view. Here is where my new role as FLoC General Chair would interact with my role as CADE trustee. That interaction, I believe, would be fruitful for both CADE and FLoC.

Apart from these political issues that I can't escape at my age my heart is still beating for research. And consequently I remain seeing it as one of my main tasks to help maintaining the high scientific standards of the CADE conferences. Research presented at CADE should not be classified as theoretical or practical or applied, it should only be classified as good or bad, and excellency should be the only criterion according to which we decide what is CADE and what it is not.

I feel it is important that the automated reasoning community remains cohesive, despite the multitude of conferences on the topic (among which CADE, Tableaux, FTP, TPHOLs, RTA, LPAR). To this end, the idea of a periodic, but not annual, IJCAR conference seems to be a good way of getting people from all branches of automated reasoning to meet from time to time.

It is is equally important that automated reasoning displays its value in applications, and more generally its many links with other domains of logics, mathematics, and philosopy. In this respect, I will favor the move to have CADE associated workshops---which, as far as I know, were introduced this year in the context of FLoC, and should be continued even independently of FLoC.

During my career, I have been interested in several aspects of logic: automated reasoning in classical logic to begin with, then lambda-calculi, modal and intuitionistic logics, and then first-order logic again, in particular the relationship between decidable subclasses and finite tree automata. I am convinced that automated reasoning is not only a rich domain but also still a very promising one in many respects. If elected, I'll make every effort to promote it and its leading conference, CADE.

But I think this is not enough, we also need new paradigms. As an example, consider fully automated proof search for first-order logic, where I am most competent. This important subfield of automated reasoning seems completely closed. There is a small number of sophisticated high-performance systems, newcomers have no chance to enter and consequently new paradigms cannot arise. Yet it should be clear to anybody that with the general approach of those systems (organising proof search on the microscopic level of single inferences) really hard problems cannot be solved fully automatically, even if we increase the performance by magnitudes. As a trustee I would try to act in the direction that new interesting ideas which conflict with the standard approaches can be presented.

I want to conclude with something completely different. I am fully aware that in the organisation of a conference inevitably certain compromises have to me made, but nevertheless I think that it is not a law of nature that scientists have to eat bad food.

*Brief bio:* Toby Walsh recently moved to University College Cork as
SFI Research Professor and Deputy Director of the Cork Constraint
Computation Centre. He was previously an EPSRC advanced research
fellow at the University of York. He completed his Ph.D. in automated
reasoning at the University of Edinburgh under the supervision of
Profs. Alan Bundy and Fausto Giunchiglia.

(Secretary of AAR and CADE) E-mail: mariapaola.bonacina@univr.it

Over the summer I moved from the University of Iowa to the Università degli Studi di Verona, so that the AAR has now a home in Verona, Italy, in addition to its first home at the Argonne National Laboratory with AAR President Larry Wos and AAR Newsletter Editor Gail Pieper. It follows that the CADE Board of Trustees has a new e-mail address at

CADE-board@sci.univr.it

As far as membership is concerned, our association continues doing very well with 578 members (as of September 12, 2002) up from 553 of last year. CADE-18, held as part of the Federated Logic Conference 2002 in Copenhagen, Denmark, brought 40 new AAR members, out of 126 registered participants. The list of members is available on the Web, reachable from the AAR home page, and directly at the Web site.

All members are encouraged to consult this list, and send by e-mail corrections and additions, especially the url of their home page, if missing. The list of members on the Web will be updated at least once per year, as time permits.

**Author:** Silvio Ranise

**Institution:** LORIA & INRIA-Lorraine

**Current Web page:** http://www.loria.fr/~ranise

**Abstract:**
The thesis proposes three techniques to build reasoning specialists,
to widen their scope, and to incorporate them in the simplification
process of many verification systems.

The first contribution is a uniform methodology to build satisfiability procedure for theories which extends the theory of equality and can be axiomatized by clauses. The methodology is developed in the rewriting framework which allows us to use a standard (refutation complete) superposition-based inference system for clausal equational logic. This allows us not only to handle pure equality but also several interesting axiomatic theories that were not handled previously that way such as lists, extensional arrays, and finite sets with extensionality. The proof that the decision procedures are correct is straightforward w.r.t. other correctness proofs given in the literature. In our approach, deriving satisfiability procedures for combination of theories is also immediate.

The second contribution is a technique to extend the capabilities of reasoning specialists so that they can be linked with general-purpose verification system in a productive way. More precisely, given a satisfiability procedure for a class of formulae C, we describe how to widen its scope so that the satisfiability problem of a class C', which is a superset of C, can be (semi-)decided by the available procedure for C. The key ingredient of the extension schema is a lemma speculation mechanism that `reduces' the satisfiability problem of C' to the satisfiability problem of C. The schema enjoys basic theoretical properties such as soundness and termination.

The third contribution is a (tight) integration schema between conditional rewriting and a satisfiability procedure. Rewriting is one of the most important formula simplification mechanism for theorem provers. The key observation is that contextual rewriting can be obtained by combining traditional conditional rewriting with a procedure capable of deciding whether any given literal is entailed by the context and normalizing expressions w.r.t. the information available in the context. Furthermore the pattern of interaction between rewriting and the procedure does not depend on the theory decided by the procedure. Constraint Contextual Rewriting (CCR, for short) is then the result of abstracting contextual rewriting from the theory decided by the decision procedure employed. An implementation of CCR, called Rewrite and Decision Procedure Laboratory (RDL), is described together with the experimental results on a corpus of significant problems extracted from the literature.

**Author:** Aaron Stump

**Institution:** Stanford University

**Date submitted:** August 2002

**Current Web page:** http://www.cs.wustl.edu/ stump/

**Abstract:**
In automated reasoning, *decision procedures* are algorithms
capable of reporting whether or not a formula is logically valid.
Decision procedures are fundamental tools for formal verification and
other applications. This thesis describes solutions to theoretical
and engineering problems arising in the development of the CVC
(``Cooperating Validity Checker'') decision procedure. CVC implements
a framework that allows independent decision procedures for the
quantifier-free consequences of different logical theories to be
combined. Assuming certain properties of those decision procedures,
the combination results in a sound and complete decision procedure for
the quantifier-free consequences of the combined theory. There are
currently decision procedures implemented for theories of arrays,
linear real arithmetic, and inductive data types.
See the
CVC
Web page.

The thesis begins with an overview of the internals of CVC. Then CVC's array decision procedure is described. This is the first published procedure for its theory, which subsumes similar theories previously decided in the literature. Next, an approach is described for handling partial functions. The approach is based on a theorem reducing validity in a logic of partial functions to validity in classical logic. Then proof production in CVC is considered. CVC has the ability to produce a proof for every formula it reports to be valid. These proofs are produced in a proof meta-language based on the Edinburgh Logical Framework (LF). The proofs can be checked by a proof checker called flea. Several new language features are supported in flea that make it much easier to produce proofs from CVC. Also, flea implements new optimizations to the basic LF type-checking algorithm to be able to check the large proofs produced by CVC for large input formulas. Empirical results showing the benefits of the optimizations are presented. Finally, several uses of proofs beyond certifying correctness of CVC's results are described, including a technique which extracts information from proofs to feed back to CVC's propositional reasoning engine, the Chaff SAT solver, for improved performance.

*Isabelle/HOL: A Proof Assistant for Higher-Order Logic*

by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel

Springer LNCS 2283, ISBN 3-540-43376-7

Web site

This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts:

*Elementary Techniques*shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion.*Logic and Sets*presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes Isabelle/HOL's treatment of sets, functions, and relations and explains how to define sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.*Advanced Material*describes a variety of other topics. Among these are the real numbers, records, and overloading. Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an extended example: the verification of a security protocol.

We are seeking articles on
**Bytecode Verification**
for a special issue of the *Journal of Automated Reasoning.*

**Topics:** Bytecode verification for the Java Virtual Machine and related
approaches to program analysis of low-level code for the enforcement of
safety properties. Particularly welcome are contributions emphasizing the
correctness of the analysis and the application of automated or interactive
verification techniques.

**Submissions:** Manuscripts should be unpublished works and not
submitted elsewhere. Revised and enhanced versions of papers
published in conference proceedings that have not appeared in
archival journals are eligible for submission. All submissions will
be reviewed according to the usual standards of scholarship and
originality.

**Deadline for submissions**: October 13, 2002.

**Guest editor:** Tobias Nipkow (nipkow@in.tum.de)

For further information see the Web site.

During the past ten years, theorem proving has been playing
an increasingly important role in education.
One reason is the improvement in the "friendliness" of theorem provers;
many are now suitable for the nonspecialist and produce quite readable proofs.
Another is their demonstrated success in solving
not only "toy" problems but previously open questions in mathematics and logic
.
In light of these developments, we plan a special issue of
the *Journal of Automated Reasoning,* ARTE, on
the use of theorem provers in education at all levels.

**Editor:**

Deepak Kapur, University of New Mexico

**Topics**

Possible topics include the following:

We welcome contributions about experiences using automated theorem provers for education at all levels: from elementary and secondary school to college and university and beyond.

Our focus is not on the use of theorem provers in classes specifically devoted to the teaching of theorem proving or automated reasoning. Rather, we are especially interested in discussion of the benefits (or problems encountered) in using automated theorem proving technology to motivate students and to enhance their ability to understand new topics.

Prospective contributors are welcome to contact the editor to discuss the suitability of topics and papers.

** Submission**

Please send 3 copies of your manuscript or (preferably) a postscript file to

Chairperson, Computer Science Department

University of New Mexico

Albuquerque, NM 87131

E-mail: kapur@cs.unm.edu

Managing Editor, Journal of Automated Reasoning

Mathematics and Computer Science Division

Argonne National Laboratory

Argonne, IL 60439

E-mail: pieper@mcs.anl.gov

**Timetable**

Submission deadline: December 10, 2002

Notification: May 10, 2003

*Conference Chairs*:
Geoff Sutcliffe (University of Miami, USA) and
Jeff Pelletier (University of Alberta, Canada)

*Program Chair*:
Franz Baader (TU Dresden, Germany)

More details will soon be available on the conference Web page.

Proposals should include the following:

- A short scientific summary and justification of the proposed topic. This should include a discussion of the particular benefits of the topic to the LICS community.
- A discussion of the proposed format and agenda, the proposed duration (this may vary from half a day to two days), and preferred dates.
- Procedures for selecting participants and papers.
- Expected number of participants.
- Potential invited speakers.
- Plans for proceedings or other publications.

Proposals are due Nov. 1, 2002, and should be submitted electronically to Prakash Panangaden, Workshops Chair LICS'03 (prakash@cs.mcgill.ca).

For further information, see the LICS Web site.

As computers become more powerful, their ability to perform complicated reasoning tasks increases. To harness their power, we need to understand the reasoning they do, and how they may do it more efficiently. This understanding begins with logic.

The Australian National University (ANU) has an exciting opportunity for IT professionals, senior educators, and students to enhance their logic and reasoning skills for the workforce, for teaching, or for higher degree by research study, in a two-week intensive summer school at the ANU.

The Logic and Automated Reasoning Summer School, to be held on 2-13 December 2002, comprises a blend of practical and theoretical short courses on aspects of pure and applied logic taught by international and Australian experts. The school provides a unique learning experience for all participants, backed up with state-of-the-art computational science facilities at the ANU.

The school is most suitable for

- IT professionals using formal methods or problem-solving technologies;
- Senior educators who teach logic at all levels;
- Postgraduate and undergraduate students who are going on to research logic or related fields in computing, mathematics, or philosophy.

**Fees:**

*Professionals:*$1,650 per person. Discounts are available for multiple registrations from individual companies and institutions.*Students in full-time education:*$120 per person. Scholarships are available and are assessed on a case-by-case basis. The Web site has more details.

**Registration:** Closes Friday, 1 November 2002.
Registrations after this date will attract a 20 percent surcharge.

Visit the Web site for more information. To discuss this invitation in more detail, including advice on suitable candidacy, please contact John Slaney at the Automated Reasoning Group:

Email lss-admin@arp.anu.edu.au; phone +61 2 6125 8630; fax +61 2 6125 8651

Gail Pieper 2002-09-11