NEWSLETTER
From the AAR President
Boyer, Kaufmann, and Moore Win 2005 ACM Software System Award
Bibel Wins Herbrand Award
Woody Bledsoe Student Travel Award
Call for Nominations: CADE Trustees Election
Satisfiability Modulo Theories Competition
Call for Abstracts of Theses
ESSLLI 2007: Call for Course and Workshop Proposals
Call for Papers:
Journal of Logic and Computation Special Issue
Conference Calls for Papers
From the AAR President, Larry Wos...
I am delighted to start this issue of the AAR Newsletter with
the announcement of two awards: one to Wolfgang Bibel, and
the other to
Robert Boyer, Matt Kaufmann, and J Strother Moore.
Congratulations to all!
For those who are now motivated to try for other awards,
I mention two that are featured in this issue:
a student travel award for FLoC and
an SMT competition for CAV'06. Both
events will take place in Seattle, Washington, in mid-August.
We are proud to announce that
Robert Boyer, Matt Kaufmann, and J Strother Moore have won
the
ACM Software System Award for 2005 for the
development and application of
the Boyer-Moore Theorem Prover.
The Software System Award is given to an institution or individuals recognized for developing a software system that has had a lasting influence,
reflected in contributions to concepts, in commercial acceptance, or both.
The Boyer-Moore Theorem Prover developers were honored
``for pioneering and engineering a most effective
theorem prover ... as a formal methods tool for verifying safety-critical
hardware and software.''
The award carries a prize of $10,000 provided by IBM.
It is my distinct honor to announce on behalf of the Board of Trustees
of CADE Inc. that Wolfgang Bibel
is to receive the
2006 Herbrand Award for Distinguished Contributions to Automated Reasoning
in recognition of his seminal work on first-order theorem proving and its
applications in artificial intelligence and programming.
His research on the connection method laid the foundations for many modern
deduction systems, and it had significant influence on other research areas
such as logic programming, knowledge representation, and deductive planning.
The Woody Bledsoe Student Travel Award was created to honor the memory
of Woody Bledsoe, for his contributions to mathematics, artificial
intelligence, and automated theorem proving, and for his dedication to
students.
The award is intended to enable selected students to attend the
International Conference on Automated Deduction (CADE) or the
International Joint Conference on Automated Reasoning (IJCAR),
whichever is scheduled for the year, by covering much of their
expenses.
In 2006, IJCAR will take place from August 17 through 20, in Seattle,
Washington, USA, as part of the Federated Logic Conference (FLoC).
For further information see
the
Web page.
The winners will be reimbursed (up to some maximum amount to be
determined, usually around US$ 500-750) for their conference
registration, transportation, and accommodation expenses. Preference
will be given to students who will play an active role in the
conference, including satellite workshops, and do not have alternative
funding. However, students in other situations are also much
encouraged to apply. A nomination consists of a recommendation letter
of up to 300 words from the student's supervisor. Nominations for
IJCAR 2006 should be sent by e-mail to Peter Baumgartner
(Peter.Baumgartner@nicta.com.au)
by June 15, 2006.
The winners will be notified by June 30 (the early registration
deadline for FLoC'06 is July 10). The awards will be presented at
IJCAR; in case a winner does not attend, the chairs and trustees may
transfer the award to another nominee or give no award.
Nominations for three CADE trustee positions are being sought, in
preparation for the elections to be held this coming fall.
The board of trustees currently includes (in alphabetical order):
The terms of Franz Baader, Peter Baumgartner, and Michael Kohlhase
expire after IJCAR 2006, because CADE trustees are elected for three
years. The term of office of Uli Furbach as program chair of IJCAR
2006 also ends.
Among the outgoing trustees, Franz Baader and Peter Baumgartner are
eligible to be nominated for a second term. Uli Furbach as outgoing
ex-officio trustee is also eligible to be nominated for a first term
as an elected trustee.
Nominations can be made by any AAR member, either by e-mail or in person
at the IJCAR 2006 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 CADE
Web site.
E-mail nominations are to be sent to Franz Baader, CADE President
(baader@tcs.inf.tu-dresden.de) and Amy Felty, CADE Secretary
(afelty@site.uottawa.ca), by the end of IJCAR 2006 (August 21, 2006).
Decision procedures for checking satisfiability of logical formulas are crucial
for many verification applications. Of particular recent interest are solvers
for Satisfiability Modulo Theories (SMT). SMT-COMP aims to spur innovation in
SMT research by providing a yearly friendly competition for SMT solvers.
SMT-COMP came out of discussions surrounding the SMT-LIB initiative, an
initiative of the SMT community to build a library of SMT benchmarks in a
proposed standard format. SMT-COMP helps serve this goal by contributing
collected benchmark formulas used for the competition to the library and by
providing an incentive for implementors of SMT solvers to support the SMT-LIB
format.
The methodology and the results of the competition will be presented at the end
of CAV'06, which will take place in Seattle, Washington, USA, August 16-20, 2006.
A more detailed discussion of the competition will take place in a
special SMT-COMP meeting the evening of August 20.
Benchmarks
The potential benchmark divisions for this year will include all of the
divisions represented last year as well as several new ones. For detailed
descriptions of the divisions, refer to the SMT-LIB
Web page.
Important Dates
The organizers are
Clark Barrett (New York University, barrett@cs.nyu.edu),
Leonardo de Moura (SRI International, demoura@csl.sri.com), and
Aaron Stump (Washington University in St. Louis, stump@cse.wustl.edu).
For details on the competition, see
the
Web page.
For more information on the smt-lib format, see
the
site.
Since 2000, the AAR Newsletter has published the abstracts
of new doctorate theses in automated reasoning.
We encourage you to submit your own abstract or to invite your students
to submit the information.
The abstract should indicate authors and title of the thesis,
name of the advisor, date of defense and institution granting the degree,
and it should provide a brief summary of the thesis, including
its table of contents.
Please submit the
abstracts to Gail Pieper, AAR Newsletter Editor,
at pieper@mcs.anl.gov.
The 19th European Summer School in Logic, Language and Information (ESSLLI)
will take place in Dublin, Ireland, August 6-17, 2007.
ESSLLI offers foundational, introductory, and
advanced courses, as well as workshops, covering a wide variety of
topics in three areas: Language and Computation,
Language and Logic, and Logic and Computation.
Courses are taught by 1 or 2 lecturers. Courses
consist of five sessions (a one-week course), each session lasting 90
minutes. Lecturers who want to offer a long, two-week course should
structure it as two independent one-week courses (ideally, with an
introductory part in the first week of ESSLLI, and a more advanced part
during the second). The ESSLLI program committee has the right to
select only one of the two proposed courses.
Timetable for Course Proposal Submission
June 15, 2006: Proposal Submission Deadline
Foundational Courses:
These are strictly elementary courses not
assuming any background knowledge. They are intended for people to
get acquainted with the problems and techniques of areas new to them.
Ideally, they should allow researchers from other fields to acquire
the key competences of neighboring disciplines, thus encouraging the
development of a truly interdisciplinary research community.
Foundational courses may presuppose some experience with scientific
methods in general, so as to be able to concentrate on the issues
germane to the area of the course.
Introductory Courses:
Introductory courses are central to the
activities of the Summer School. They are intended to equip students
and young researchers with a good understanding of a field's basic
methods and techniques. Introductory courses in, for instance,
Language and Computation, can build on some knowledge of the component
fields; for example, an introductory course in computational linguistics
should address an audience familiar with the basics of
linguistics and computation. Proposals for introductory courses should
indicate the level of the course as compared to standard texts in the
area (if available).
Advanced Courses:
Advanced courses should be pitched at an audience of
advanced master's or Ph.D. students. Proposals for advanced courses
should specify the prerequisites in detail.
Workshops:
The aim of the workshops is to provide a forum for advanced
Ph.D. students and other researchers to present and discuss their
work. Workshops should have a well defined theme, and workshop
organizers should be specialists in the theme of the workshop.
Organizers must give a general introduction to the
theme during the first session of the workshop. They are also
responsible for the organization and program of the workshop including
inviting the submission of papers, reviewing, expenses of invited
speakers, and so forth. Each workshop organizer will be responsible for
producing the 1st Call for Papers in December 2006. The call must
make it clear that the workshop is open to all members of the LLI
community. It should also note that all workshop contributors must
register for the Summer School.
Workshop proposals must be submitted by June 15, 2006.
Notice that workshop speakers will be required to register for the
Summer School; however, they will be able to register at a reduced
rate to be determined by the local organizers.
A Web-based form for submitting course and
workshop proposals is accessible at
the
Web site.
Finances:
All teaching and organizing at the summer schools
is done on a voluntary basis in order to keep the participants' fees as
low as possible. Lecturers and organizers are not paid for their
contribution but are reimbursed for travel and accommodation (up to a
fixed, maximum amount that will be notified to lecturers when courses
are accepted).
The local organizers highly appreciate it if, whenever possible,
lecturers and workshop organizers find alternative funding to cover
travel and accommodation expenses. Such issues might be taken
into account when selecting courses.
We stress that while proposals from all
over the world are welcomed, the Summer School cannot guarantee full
reimbursement of travel costs, especially from destinations outside
Europe.
Please note the following: If a course is to be taught by two
lecturers, a lump sum is reimbursed to cover travel and accommodation
expenses for one lecturer. The splitting of the sum is up to the
lecturers.
Chair: Tomaz Erjavec, Jozef Stefan Institute,
Jamova 39, SI-1000 Ljubljana, Slovenia
(e-mail: tomaz.erjavec@ijs.si;
www: http://nl.ijs.si/et/).
The Web site for ESSLLI 2007 will become
operational in the second half of 2006. For this year's summer school,
please see the
Web site.
Researchers are
cordially invited to submit articles for a special issue of the
Journal of Logic and Computation
on natural language and knowledge representation.
Natural language processing (NLP) and the knowledge
representation (KR) communities have common goals.
They are both concerned
with representing knowledge and with reasoning, since the best test for the
semantic capability of an NLP system is performing reasoning tasks. Having
these two essential common grounds, the two communities ought to have been
collaborating, to provide a well-suited representation language that covers
these grounds. However, the two communities also have difficult-to-meet
concerns. Mainly, the semantic representation (SR) should be expressive
enough and take the information in context into account, while the KR should
be equipped with a fast reasoning process.
The main objection against using an SR or a KR is that they need experts to
be understood. Nonexperts communicate (usually) via a natural language
(NL), and more or less they understand each other while performing a lot of
reasoning. An essential practical value of representations is their attempt
to be transparent. This will particularly be useful when or if the system
provides a justification for a user or a knowledge engineer on its line of
reasoning using the underlying KR (i.e., without generating back to NL).
We all seem to believe that, compared to natural language, the existing
knowledge representation and reasoning systems are poor. Nevertheless, for a
long time, the KR community has dismissed the idea that NL can be a KR.
That's because NL can be very ambiguous and there are syntactic and semantic
processing complexities associated with it. However, researchers in both
communities have started looking at this issue again. Possibly, it has to do
with the NLP community making some progress in terms of processing and
handling ambiguity, the KR community realizing that a lot of knowledge is
already "coded" in NL and that one should reconsider the way they handle
expressivity and ambiguity.
For this special journal issue of logic and computation, we invite the
submission of original, high-quality articles. Topics for this special
issue include the following:
The deadline for paper submissions (max. 20 pages, pdf) is July 31, 2006.
For advice on topic, scope, and suitability for the special issue, or
to submit papers electronically, please contact
Jana Sukkarieh (j.sukkarieh.94@cantab.net).
The submission process
also will be soon available on
the
Web.
The articles will be
peer reviewed, and notification for authors will be sent as soon as possible
after the date of submission.
As with last year, we reserve the right to remove benchmark divisions if we do
not receive enough quality benchmarks or enough solvers in a particular
division. If you have access to benchmarks in any of these divisions, even if
they are not in the SMT-LIB format, please contact one of the organizers (see
below).
Journal of Logic and Computation
Special Issue on Natural Language and Knowledge Representation
| program verification | program certification |
| model checking | debugging techniques |
| abstract interpretation | abstract domains |
| static analysis | type systems |
| deductive methods | optimization |
Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. The proceedings will be published by Springer in the Lecture Notes in Computer Science series.
The page limit for submissions is 15 pages in Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewer. Formatting style files can be found at the Web site. The submission deadline is September 8, 2006.
For further information, see the Web site.
| CAV | Conference on Computer Aided Verification (Aug 17-20) |
| ICLP | Int'l Conference on Logic Programming (Aug 17-20) |
| IJCAR | Int'l Joint Conference on Automated Reasoning (Aug 17-20) |
| LICS | IEEE Symposium on Logic in Computer Science (Aug 12-15) |
| RTA | Conference on Rewriting Techniques and Applications (Aug 12-14) |
| SAT | Int'l Conference on Theory and Applications of |
| Satisfiability Testing (Aug 12-15) |
The FLoC'06 program includes a keynote session to commemorate the Goedel Centenary, with John Dawson and Dana Scott as speakers; a keynote talk by David Harel; plenary talks by Randy Bryant and David Dill; and several invited talks.
FLoC has received an NSF grant to provide funds for travel grants of up to $750 for student attendees of FLoC'06. We expect to award about 50 grants. See application information on the Web site.
Online registration for FLoC is now open at the Web site.
The deadline for preferred hotel rate is June 21, 2006; the deadline for early registration is July 10, 2006.
MICAI 2006
The 5th Mexican International Conference on Artificial Intelligence
will take place
November 13-17, iin Mexico.
Papers accepted for oral presentation will be published by Springer in
Lecture Notes in Artificial Intelligence. Papers accepted
for poster sessions will be published by IEEE CS Press.
Submissions must be received via
the
Web site
by June 2, 2006.
LFCS'07
The Symposium on Logical Foundations of Computer Science
will take place in
New York City, June 4-7, 2007.
The LFCS series provides an outlet for the fast-growing body
of work in the logical foundations of computer science, for example, areas of
fundamental theoretical logic related to computer science.
Topics of particular interest to AAR members include
logic
programming and constraints; automated deduction and interactive theorem
proving; logical methods in protocol and program verification;
term
rewriting;
intelligent and multiple agent system logics; logics of proof and
justification; and nonmonotonic reasoning.
Submissions must be made electronically (15 pages, according to
LNCS standards) to lfcs07@gmail.com, by
December 18, 2006.
For more information, see the
Web page.
TABLEAUX 2007
TABLEAUX 2007,
Automated Reasoning with Analytic Tableaux and Related Methods,
will take place
July 3-6, 2007, in Aix en Provence, France.
The PC chair is Nicola Olivetti, LSIS, Paul Cézanne University, Marseille, France.
Gail Pieper
pieper@mcs.anl.gov
June 2006