From the AAR President, Larry Wos...
Kudos and comments: I am delighted at the excellent work of our secretary Maria Paola Bonacina in obtaining up-to-date e-mail addresses for our members. Please read her article to learn about changes in the AAR membership and how these changes may affect you.
As she notes, we view the AAR newsletter as a mechanism for scientific exchange. We want your contributions: do you have an open question, an exercise in automated deduction that you have found useful with students, a new reasoning program? Or do you have a problem you would like to have solved? (I especially enjoy trying to find shorter proofs for challenging problems.) Please send these to our newsletter editor Gail Pieper (pieper@mcs.anl.gov).
Many of you were at the CADE-15 conference in Lindau, Germany,
and had the opportunity to attend the various workshops
offered.
For those who wish more information about those workshops, we
give here the links to the appropriate Web sites.
Problem-Solving Methodologies with Automated Deduction
Proof Search in Type-Theoretic Languages
Strategies in Automated Deduction
Integration of Deduction Systems
Automation of Proof by Mathematical Induction
Mechanization of Partial Functions
Tableaux'99
Tableaux'99, an international conference on
analytic tableaux and related methods,
will take place on June 8-11, 1999, at
Saratoga Springs, New York.
Tableau methods have been found to be a convenient formalism for
automating deduction in various nonstandard logics as well as in
classical logic. Areas of application include verification of software
and computer systems, deductive databases, knowledge representation
and its required inference engines, and system diagnosis. The
conference brings together researchers interested in all aspects-theoretical
foundations, implementation techniques, systems
development and applications-of the mechanization of reasoning with
tableaux and related methods.
The conference will include contributed papers, tutorials, system
descriptions, a poster session, and invited lectures.
A special feature will be
a comparison of theorem provers.
This comparison is organized by Fabio Massacci of
Universita di Roma ``La Sapienza".
For information, send e-mail to
massacci@dis.uniroma1.it.
Topics of interest include the following:
Submissions are
invited in three categories:
(A) Original research papers (up to 15 pages),
(B) Original papers on system descriptions (up to 5 pages),
and (C) Tutorials in all areas of analytic tableaux and related methods
from academic research to applications (proposals up to 5 pages).
The conference proceedings
(including accepted papers of categories A and B) will be
published within the LNAI series of Springer.
Tutorial submissions (category C) may be at introductory,
intermediate, or advanced levels. Novel topics and topics of broad
interest are preferred.
Authors are requested to submit via email in PostScript to the Program
Chair Neil V. Murray (tab99@cs.albany.edu) by December 4, 1998.
Additional information is available through WWW address:
http://www.cs.albany.edu/ nvm/tab99/.
The second Federated Logic Conference (FLOC'99) will be held in Trento, Italy,
in July 1999.
Four conferences will participate in FLoC:
Conference on Automated Deduction (CADE),
Conference on Computer-Aided Verification (CAV),
IEEE Symposium on Logic in Computer Science (LICS), and
Conference on Rewriting Techniques and Applications (RTA).
LICS 99
The Fourteenth Annual IEEE Symposium on
Logic in Computer Science will take place on
July 2-5, 1999, in Trento, Italy.
The LICS Symposium is an annual international forum on theoretical and
practical topics in computer science that relate to logic in a broad
sense.
Topics of interest include abstract data types, automated deduction,
bounded arithmetic, categorical models and logics, combination of
logics, concurrency, constraint programming, constructive mathematics,
database theory, denotational semantics, domain theory and
applications, finite model theory, formal methods, game semantics,
hybrid systems, logics of knowledge, lambda and combinatory calculi,
linear logic, logical aspects of computational complexity, logics in
artificial intelligence, logics of programs, logic programming, modal
and temporal logics, model checking, logical aspects of protocol
security, rewriting, semantics, software specification, type theory
and type systems, universal algebra, and verification.
Authors should send
an extended abstract
to the program chair, Giuseppe.Longo@ens.fr, and to the associate chair,
Gilles.Dowek@inria.fr, by December 10, 1998.
Of special interest is the
Kleene Award for Best Student Paper, an award of $500to be given for the best student paper, as judged
by the program committee.
For more information,
see http://www.cs.bell-labs.com/cm/cs/what/floc99.
RTA 99
The Tenth International Conference on Rewriting Techniques and
Applications will take place July 2-4, 1999, in
Trento, Italy, as part of the Federated Logic Conference
FLoC'99 (http://www.cs.bell-labs.com/cm/cs/what/floc99).
Papers are solicited in any of the following or related areas:
In addition to full research papers (15 pages), descriptions of new working
systems (4 proceedings pages) and problem sets that provide
realistic, interesting challenges in the field of rewriting
techniques are also welcome. High-quality papers on new
applications of rewriting techniques are particularly encouraged.
Submissions must reach the program chairmen by December 1, 1998.
The conference proceedings will be published by Springer-Verlag
as part of their Lecture Notes in Computer Science series.
For further information, see
http://rta99.loria.fr/
CADE-16
CADE is the major forum for presentation of research in all aspects of automated
deduction.
CADE-16 will take place July 7--10, 1999,
in Trento, Italy, as part of FLoC'99.
Original research papers and descriptions of
working automated deduction systems are solicited.
Logics of interest include propositional, first-order, equational, higher-order,
classical, intuitionistic, constructive, nonstandard, and
meta-logics, and type theory. Methods of interest include saturation, tableaux,
term rewriting, induction, unification, constraint solving,
decision procedures, model generation, model checking, logical frameworks, and A
I-related methods for deductive systems such as
proof planning and proof presentation. Applications of interest include hardware
and software development, systems analysis and
verification, deductive databases, functional and logic programming, computer ma
thematics, and deduction for natural language
processing and other AI areas. Special topics of interest include proof theory,
human-computer interfaces, distributed deduction, and
search and simplification heuristics.
Research papers can be up to 15 proceedings pages, and system descriptions can b
e up to 4 pages. The
proceedings of CADE-16 will be published by Springer-Verlag in the LNAI series.
Papers should be compressed, then uuencoded, then e-mailed to the program chair
Harald Ganzinger,
Max-Planck-Institut für Informatik,
Im Stadtwald,
66123 Saarbrücken,
Germany;
Phone: +49 681 9325 201;
FAX: +49 681 9325 299;
E-mail: cade-16@mpi-sb.mpg.de.
All submissions must be received by January 5, 1999.
Details on the procedure and alternatives can be
found at the CADE-16 Web site www.mpi-sb.mpg.de/cade-16/cfp.html.
CAV'99
CAV'99 is the eleventh in a series dedicated to the advancement of the theory an
d practice of computer-assisted formal analysis methods
for software and hardware systems.
The conference covers the spectrum from theoretical results to concrete applicat
ions, with an
emphasis on practical verification tools and the algorithms and techniques that
are needed for their implementation.
The topics of interest include
modeling and specification formalisms,
algorithms and tools,
(such as
model checking, synthesis, and automated deduction),
verification techniques,
applications and case studies,
and
testing based on verification technology.
Authors must submit papers by January 3, 1999.
The proceedings of the conference will be published in the Springer-Verlag Lectu
re Notes in Computer Science series.
Please direct all inquiries about CAV'99 to cav'99@imag.fr.
A new book
Theorem Proving with the Real Numbers, by
John Harrison, has been published by Springer-Verlag.
The book may appeal to
people interested in the formalization of mathematics, computer-aided
verification, and related fields.
The following summary is taken from the publisher's Web page at
http://www.springer.co.uk/comp/books/key.html.
The book can be ordered directly from there.
CONTENTS: Introduction - Constructing the Real Numbers - Formalized
Analysis - Explicit Calculations - A Decision Procedure for Real
Algebra - Computer Algebra Systems - Floating Point Verification -
Conclusions - Logical Foundations of HOL - Recent Developments -
Bibliography - Index
200 pages
Some of the theories described are distributed in the examples directory
of the HOL Light prover, available via the Web page
Those persons interested in obtaining
the rest of the HOL code should contact the author:
http://www.cl.cam.ac.uk/users/jrh.
SAT 2000
In the 1990s, there has been an explosion of research into propositional
satisfiability (or SAT). There are many factors behind the increased interest
in this area. One factor is the improvement of search procedures for SAT.
New local search procedures like GSAT and WalkSAT are able to solve SAT
problems with thousands of variables. At the same time, implementations of
complete search algorithms like Davis-Putnam have been able to solve open
mathematical problems. Another factor is the identification of hard SAT
problems at a phase transition in solubility. A third factor is the
demonstration that we can often solve real world problems by encoding them
into SAT. The 1990s have also seen an improved theoretical understanding
of SAT, particularly in the analysis of phase transition behaviour. In light
of this, there will be a special issue of the Journal of Automated Reasoning,
SAT 2000, on the state of the art for research into satisfiability as we move
into the year 2000.
Topics
We will consider empirical, theoretical or application oriented papers about
SAT. Possible topics include (but are not limited to) the following:
Algorithms
Analysis
Applications
Extensions
Prospective contributors are warmly invited to contact either, or both, of
the guest editors to discuss the suitability of topics and papers. We
especially welcome papers that discuss practical applications. In addition
to presenting new research, all papers should provide a brief summary
of their area so that outsiders can have an overview of the state of research
into SAT at the start of the new millennium.
Submission
Please send 3 copies of your manuscript or (preferably) a postscript file to
Dr. Ian Gent
Timetable
To ensure topicality of the special issue, submissions, reviewing and
revision of papers will be held to very fixed and tight deadlines.
To help us achieve this tight timetable, we have approached eminent researchers
to form a review panel, although final decisions on papers will rest with
the guest editors in collaboration with the editor of JAR. We will also
expect authors of submitted papers to help with reviewing to this timetable.
Review Panel
Maria Paola Bonacina
I have been the secretary of the Association for Automated Reasoning
for one year, and the time has come to update everyone on the state
of the association.
As of September 30, 1998, the association counts 291 members,
all of whom have a valid e-mail address.
One year ago we had 338 members, but only 277
valid e-mail addresses, which means part of my work this year has been
to reorganize the records, making sure that the newsletter reaches
as many people as possible and pruning obsolete data.
I am happy to welcome 42 new members who enrolled during 1998
for the first time, and because many of them joined by registering to CADE-15,
many thanks go to Wolfgang Bibel and the CADE-15 organizing committee for the
excellent work done in Lindau.
Now that our basic records have been put in order, I would like to extend
them by collecting the URL's of the home pages of members on the Web.
This is done on a purely voluntary basis: if members wish to
include their URL's in their AAR records, they can send
them to me at bonacina@cs.uiowa.edu.
On another side, I have been looking into augmenting the scientific contents
of the AAR newsletter. For this purpose, I proposed to include in the
newsletter the Web pages of the CADE workshops. By following the links
in this issue, readers can access all papers, abstracts, and position papers
that were presented at the CADE-15 workshops in Lindau.
Many thanks go to the workshop organizers for
making this
possible by
maintaining the Web pages.
I also would like to encourage all members to send contributions,
and help us make our newsletter a primary vehicle for the rapid
diffusion of scientific communications in our field.
Based on the consideration that the publication of the newsletter on
the World Wide Web has annulled all postage costs for the association,
the AAR officers (President Larry Wos, Vice-President Hans-Jurgen Ohlbach,
Treasurer Larry Henschen and I) agreed that
the AAR will no longer collect dues from its members.
New members enroll by sending their data to the
secretary,
while existing members are kindly requested to confirm their
membership annually, also by e-mail to the secretary.
All members
have the responsibility of keeping their data
with the association up to date,
informing the secretary of address or affiliation changes by e-mail.
Similarly, members should inform the secretary by e-mail
if they wish to leave the association.
Since September marks in many ways the beginning of a new year
(at least in academia), I would like to conclude with best wishes
for another year of good work and achievement in automated reasoning.
Abstracts and Links to the CADE-15 Workshops
Call for Papers
FLoC
New Book
Theorem Proving with the Real Numbers discusses the formal development
of classical mathematics using a computer. It combines traditional
lines of research in theorem proving and computer algebra and shows
the usefulness of real numbers in verification. This book aims to show
that a theory of real numbers is useful in practice as well as
theoretically interesting, and that the `LCF' style of theorem proving
is well suited to the kind of work described.
234 x hardcover
1998
3-540-76256-6
$40.00
http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html
Call for Papers:
Special Issue of the Journal of Automated Reasoning
(satisfiability at the start of the year 2000)
Guest Editors:
Ian P. Gent and Toby Walsh
University of Strathclyde
Department of Computer Science
University of Strathclyde
Glasgow G1 1XH
Scotland
E-mail: ipg@cs.strath.ac.uk
Phone: +44 141 548 4527
Fax: +44 141 552 5330
News from the AAR Secretary
Dept. of Computer Science - The University of Iowa
E-mail: bonacina@cs.uiowa.edu
Next: About this document