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
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).
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)
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.
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
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
Springer LNCS 2283, ISBN 3-540-43376-7
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:
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
Timetable
Submission deadline: December 10, 2002
CADE 19
The 19th International Conference on Automated Deduction
(CADE-19) will be held in
Miami, Florida, USA,
July 28 - August 2, 2003.
CADE-19 invites paper submissions related to all aspects of automated
deduction, including foundations, implementations, and
applications. Original research papers, papers on applications of
automated deduction methods and systems, and descriptions
of working automated deduction systems are solicited.
In addition, CADE-19 invites the submission of proposals for workshops
and tutorials, which will take place at the beginning of the conference
(July 28 and 29).
Topics
Logics of interest include propositional, first-order, equational,
higher-order, classical, intuitionistic, constructive, modal, temporal,
many-valued, substructural, description, and meta-logics, logical
frameworks, type theory and set theory.
Methods of interest include saturation, resolution, tableaux, sequent
calculi, term rewriting, induction, unification, constraint solving,
decision procedures, model generation, model checking, natural deduction,
proof planning, proof presentation, proof checking, and explanation.
Applications of interest include hardware and software development,
systems analysis and verification, deductive databases, functional and
logic programming, computer mathematics, natural language processing,
computational linguistics, robotics, planning, knowledge representation,
and other areas of AI.
Submission
Conference submission is electronic in postscript format. Submitted
papers should conform to the Springer LNCS style. In addition to papers
on foundations (15 pages), CADE encourages the submission of application
papers (10 pages), and of short system descriptions (5 pages).
Simultaneous submission to other conferences with proceedings or
submission of material that has already been published elsewhere is
not allowed. In the case of doubts on this point please contact the
program chair. Papers that are too long will not be considered.
Important Dates
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.
LICS 2003
The Eighteenth IEEE Symposium on Logic in Computer Science will be held in
Ottawa, Ontario, June 22-25, 2003. The organizers have
made arrangements for pre- and post-LICS workshops to be run in conjunction
with the main conference. Possible dates are 21st June and 26-27th June.
Researchers and practitioners are invited to submit proposals for
workshops on topics relating logic -- broadly construed -- to computer
science or related fields. Funding is available to help
defray the costs of a limited number of workshops.
Proposals should include the following:
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
Fees:
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
From the AAR President, Larry Wos...
Good researchers not only develop novel strategies, implement powerful
programs, and conduct numerous experiments, but they also keep the community informed about their accomplishments.
This newsletter features a number of calls for papers or for contributions to special issues.
I encourage you all to take advantage of these opportunities and to make your research results widely known.
Second International Joint Conference on
Maria Paola Bonacina
Automated Reasoning to be held in 2004
(mariapaola.bonacina@univr.it)
General Agreement
The Committees Supporting IJCAR 2004
Announcement of the 2002 Herbrand Award
Announcement of CADE Elections
Maria Paola Bonacina
(Secretary of AAR and CADE)
E-mail: mariapaola.bonacina@univr.it
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)
Statement by Harald Ganzinger
CADE is the major forum for the scientific exchange of new
theoretical and practical approaches to automated theorem proving
and its applications in mathematics and computer science.
In order to maintain high visibility of the field as a whole,
we have to try to keep CADE's spectrum as wide as possible
and to avoid any fragmentation of the field (and of CADE)
into small subcommunities with too narrow methods and techniques.
During the last three years as CADE trustee
I have helped in re-uniting our community and in creating IJCAR01 which
turned out to be a very successful event, convincingly
demonstrating the high quality and relevance of our field.
I will try to establish IJCAR as a regular event with even more
communities, in particular from major areas of application
of automated deduction, join us.
Statement by Jean Goubault-Larrecq
To the man-in-the-street, automated reasoning is a theoreticians' business.
Whilst that may be true, automated reasoning has acquired credentials in
becoming central in many application domains: software certification with
proof assistants, description logics and the semantic Web, decidable classes
of first-order logic and tree automata applied to cryptographic protocol
verification are a few examples that come to mind.
Statement by Reinhold Letz
Although the automated reasoning community is relatively stable,
in the last years CADE suffers from a continuous decrease in the
numbers of submissions and participants. Broadening of the scope
is certainly one possible remedy, another is the collocation or
the merging with other conferences, as worked successfully with
IJCAR and should definitely be continued.
Statement by Andrei Voronkov
In the recent years automated deduction developed into a mature
field. In traditional topics in deduction, such as resolution theorem
proving, obtaining new results is becoming increasingly difficult. At
the same time, there are very interesting areas where the methods of
automated deduction used extensively. As a consequence, there have been
a considerable shift of interest in automated deduction, as can be
witnessed by a change in topics of the papers accepted to CADE
and the success of newer meetings related to deduction, such as TPHOL,
Calculemus, and Tableaux. My point of view on the future of CADE is as
follows:
Statement by Toby Walsh
The automated reasoning (AR) community faces a number of fundamental
problems. First, there is increasing fragmentation. Events like
IJCAR (which I am proposing to host in Cork in 2004) are one
solution to this problem. However, we cannot stop there but must
embrace other closely related areas (for example, we need to join
with the satisfiability research community, in which I am very active)
that have common research problems. Second, there must be
more fresh blood brought into the field. I hope, for example, that
we can run a doctoral programme alongside IJCAR to engage PhD
students at an early stage in their studies. Third, we need to take
measures to prevent research in AR become stale and incremental. As area
chair in automated reasoning for CologNet, I am responsible for
organizing meetings at events like CADE and IJCAR to identify
grand challenges for AR. The hope is that these challenges will fire
the imaginations of both new researchers arriving into AR as well
those already long established in the field.
News from the Secretary
Maria Paola Bonacina
(Secretary of AAR and CADE)
E-mail: mariapaola.bonacina@univr.it
Thesis Abstracts
Title of Thesis 1:
On the Integration of Decision Procedures in Automated Deduction
Title of Thesis 2:
Checking Validities and Proofs with CVC and flea
Book Announcement
by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel
Web site
Special Issues of the Journal of Automated Reasoning
1. Bytecode Verification
2. Automated
Reasoning and Theorem Proving in Education (ARTE)
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
Notification: May 10, 2003
Call for Papers
January 15, 2003: Notification of acceptance of workshops and
tutorials
January 24, 2003: Deadline for electronic submission of title
and short abstract
January 31, 2003: Deadline for electronic submission
of papers
March 31, 2003: Notification of acceptance of papers
April 30, 2003: Deadline for final version of accepted papers
Logic and Automated Reasoning Summer School