NEWSLETTER
No. 74, January 2007
From the AAR President
Herbrand Award: Call for Nominations
Call for Papers
From the AAR President, Larry Wos...
This issue comes earlier than usual in the new year because we have several important announcements with early deadlines.
Of especial interest are the Herbrand Award, for experienced researchers who have made major contributions to automated reasoning,
and the Woody Bledsoe Student Travel Award, for students new to the fields of
mathematics, AI, and automated theorem proving.
The Herbrand Award is given by CADE Inc. to honor a person or group
for exceptional contributions to the field of automated deduction.
At most one Herbrand Award will be given at each CADE or IJCAR meeting.
The Herbrand Award has been given in the past to
Larry Wos (1992)
A nomination is required for consideration for the Herbrand award,
which will be given at CADE 2007.
The deadline for nominations for the Herbrand Award
is March 15, 2007.
Nominations pending from previous years must be resubmitted in
order to be considered.
Nominations should consist of a letter (preferably e-mail) of up to
2,000 words from the principal nominator, describing the nominee's
contribution, along with letters of up to 2,000 words of endorsement
from two other seconders. Nominations should be sent to
CADE-21
The 21st International Conference on Automated Deduction
will be held at the International University, Bremen, Germany
July 17-20, 2007, with workshops on July 15-16.
CADE is the major forum for the presentation of research in all
aspects of automated deduction:
Logics of interest include propositional, first-order, equational,
higher-order, classical, intuitionistic, constructive, modal, temporal,
many-valued, substructural, description, and metalogics, logical
frameworks, type theory, and set theory.
Methods of interest include resolution, tableaux, term rewriting,
induction, unification, constraint solving, SAT solving, decision
procedures, saturation, model generation, model checking, natural
deduction, sequent calculi, 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.
Invited Speakers:
Affiliated Workshops (July 15-16, 2007):
Paper Submission:
Submission is electronic in PostScript or PDF format via the EasyChair
system. Submitted papers must conform to the Springer LNCS style,
preferrably using LaTeX2e and the Springer llncs class files available
on the
Web. Submissions can be full papers,
for work on foundations, applications, or implementation techniques
(15 pages), as well as system descriptions (5 pages), for describing
publicly available systems. The proceedings will be published in the
Springer LNCS series.
Submissions are now open via
EasyChair.
Titles and abstracts are due February 16, 2007.
Full papers are due February 23, 2007.
The conference chair is Michael Kohlhase (IUB);
the workshop and tutorial chair is Christoph Benzmueller (Cambridge);
the program chair is Frank Pfenning (CMU).
Woody Bledsoe Student Travel Award:
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.
The winners of the 2007 Travel Award will be partially reimbursed for
their conference registration, transportation, and accommodation
expenses. Past awards have varied but have typically been 150-600
Euro, depending on the degree of active participation and the distance
that needs to be traveled.
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, also students in other situations are
encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words
from the student's supervisor. Nominations for CADE-21 should be sent
by e-mail to
Michael Kohlhase, CADE-21 Conference Chair (m.kohlhase@iu-bremen.de).
Nominations must arrive no later than June 1, 2007; the winners will be
notified by June 10. The awards will be presented at CADE. In case a
winner does not attend, the chairs and trustees may transfer the award
to another nominee or give no award.
ESARLT
The CADE-21 Workshop on Empirically Successful Automated Reasoning in Large
Theories (ESARLT) will bring together practitioners and researchers who are
concerned with the development and application of automated reasoning in large
theories--theories in which there are
In large theories it is useful to develop and apply intelligent reasoning
techniques that go beyond ``black box'' reasoning, to include techniques for
selecting axioms, and using proved theorems as lemmas. Reasoning in all forms
(automated, interactive, etc.) and all logics (classical, nonclassical, all
orders, etc.) is of interest to the workshop. The workshop will discuss only
``really running" systems and applications, and not theoretical ideas that have
not yet been translated into working software.
ESARLT is the successor to the successful ESFOR, ESCAR, ESHOL, and ESCoR
workshops. CADE-21 will be July 15-20, 2007.
Submission of papers for presentation at the workshop, and proposals for system
and application demonstrations at the workshop, are invited. Submissions
will be refereed, and a balanced program of high-quality contributions will be
selected. The selected contributions will be printed as workshop proceedings
and will also be published electronically. The submission deadline is May 7, 2007,
notification of acceptance is on June 8, and final versions are due
June 25. Submission information is
online.
MKM 2007
The Sixth International Conference on
Mathematical Knowledge Management will be held in Hagenberg, Austria,
June 27-30, 2007.
Mathematical knowledge management is an innovative field in the
intersection of mathematics and computer science. Its development is
driven on the one hand by the new technological possibilities that
computer science, the Internet, and intelligent knowledge processing
offer, and on the other hand by the need for new techniques for
managing the rapidly growing volume of mathematical knowledge.
The conference is concerned with all aspects of mathematical knowledge
management, including the following of particular interest to AAR members:
The deadline for submissions is February 12, 2007. Submitted papers should
not exceed 15 pages and must be original.
The proceedings will be published in the Springer-Verlag series
Lecture Notes in Artificial Intelligence.
Authors of accepted papers are expected to present their work
at the conference.
The local organizer is
Wolfgang Windsteiger (Johannes Kepler University, Linz, Austria).
For more information, see the
MKM Interest Group
or
Calculemus 2007
Web sites.
Note that there will be
affiliated workshops with the MKM and Calculemus conferences.
Those interested in organizing a workshop should contact the co-chairs Manfred Kerber and Robert Miner at mkm07@cs.bham.ac.uk.
Trends in Logic V
Trends in Logic V, a Studia Logica international conference,
will take place in
Guangzhou, China, July 6-9, 2007.
The conference seeks to bring together researchers
working in
many-valued logics, encourage
a greater degree
interaction among the featured research
communities, and act as a catalyst for new directions of research.
Contributions are welcome that concern applications of mathematical
methods to philosophical problems, especially
in the following areas:
Contributors should send
an abstract not exceeding two pages to Jacek Malinowski
(jacekm@uni.torun.pl) by April 1, 2007. Abstracts
must be submitted as Latex or MS Word files. Authors will be
notified about acceptance before May 15, 2007.
For further information, contact
the Institute of Logic and Cognition, Sun Yat-sen University
(the south campus), Guangzhou, China, 510275; fax: +86 20 8411 0298;
e-mail ICLC2007@yahoo.com.cn.
See also
the general Studia Logica
Web site and
the online
call for papers.
TABLEAUX 2007
The 16th international meeting on
Automated Reasoning with Analytic Tableaux and Related Methods
will be held in Aix en Provence, France,
July 3-6, 2007.
Tableau methods are a convenient formalism for automating deduction
in various non-standard 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 the theoretical
foundations, implementation techniques, systems development, and
applications of the mechanization of reasoning with tableaux and
related methods.
Topics include
the following:
Of particular interest are
papers describing
applications of tableaux and related methods in areas such as
hardware and software verification, knowledge engineering,
and the semantic Web.
Submissions are
invited in four categories:
Submissions in categories A and B will be reviewed by peers,
typically members of the program committee.
Accepted
papers in these categories will be published in the conference
proceedings. For category B submissions a working
implementation must exist and be available to the referees.
Submissions in category C will be reviewed by members of the
program committee, and a collection of the accepted papers in this
category will be published as a technical report of the
LSIS/Université Paul Cézanne.
Tutorial submissions in category D may be at introductory,
intermediate, or advanced levels. Novel topics and topics of broad
interest are preferred. The submission should include the title, the
author, the topic of the tutorial, its level, its relevance to
conference topics, and a description of the interest and the
scientific contents of the proposed tutorial. Tutorial proposals
will be reviewed by members of the program committee.
The deadline for submission of title and abstract is February 2, 2007.
Paper submissions are due February 9, 2007.
Authors of accepted papers are expected to present their work at the
conference.
Workshops
TABLEAUX 2007 also has launched
a call for workshop proposals on specialized
subjects in the range of the conference topics.
Up to two proposals can be accepted.
The purpose of a workshop is to offer an opportunity of presenting novel
ideas, ongoing research, and to discuss the state of the art of an area in
a less formal but more focused way than the conference itself. It is also
a good opportunity for young researchers to present their own work and to
obtain feedback. The format of a workshop is left to the organizers,
but it is expected to contain significant time for discussion.
The intended schedule is for one-day workshops.
The deadline for workshop proposal submissions is
January 31, 2007.
For more information, see the
Web site.
2007 ASL European Summer Meeting
The Logic Colloquium '07 will take place in
Wroclaw, Poland,
July 13-19, 2007.
This meeting will be collocated with the 2007 International
Colloquium on Automata, Languages and Programming (ICALP 2007; see
the ASL "other meetings" Web page and
the
EATCS Web page) and the
Twenty-Second Annual IEEE Symposium on Logic In Computer Science
(LICS 2007; see the ASL "other meetings" Web page and
LICS Web page).
Abstracts of contributed talks submitted by ASL members will be
published in the Bulletin of Symbolic Logic if they satisfy the rules
for abstracts.
Abstracts--hard copy or e-mail--should be
received before the deadline of April 17, 2007.
See the
ASL Web site
for more information.
HyLo 2007
The International Workshop on Hybrid Logic 2007
(affiliated with ESSLLI 2007)
will be held in
Dublin, August 6-10, 2007.
Hybrid logic is a branch of modal logic allowing direct
reference to worlds, times, and states.
The expressive power from hybrid logic is useful for applications.
Moreover, hybrid-logical
machinery improves the behavior of the underlying modal formalism.
The topic of HyLo 2007 is not only standard
hybrid-logical machinery such as nominals, satisfaction operators, and
the downarrow binder, but also extensions of modal logic that
increase its expressive power. HyLo 2007
Is intended for people interested in
description logic, feature logic, applied modal logics, temporal
logic, and labeled deduction.
The submission deadline is March 8, 2007.
For
Submission details, see the HyLo
Web page.
Accepted papers will appear in the workshop proceedings
published by ESSLLI.
Revised versions of
accepted papers will be published in a special issue of Journal of Logic,
Language and Information.
FTP'07
The International Workshop on
First-Order Theorem Proving
(FTP'07) will be held in
Liverpool, England,
September 12-13, 2007.
The workshop
will be collocated with the 6th
International Symposium on Frontiers of Combining Systems
(FroCos'07), which will take place prior to FTP'07.
The FTP workshop focuses on all aspects of theorem
proving in first-order logic. It aims to be a forum for the
presentation of original work and for the discussion of work in
progress.
Relevant topics for the workshop include
the following:
For more information about FTP, its scope and previous workshops, please, see
the
workshops Web page.
For regular updates about the workshop organization, please see
the
FTP'07 Web page.
To contact the PC chair, please send an email to
Silvio.Ranise[AT]loria.fr (substitute [AT] with "@").
Call for Nominations
Amy Felty
Secretary of AAR and CADE
On behalf of the CADE Inc. Board of Trustees
Woody Bledsoe (1994)
Alan Robinson (1996)
Wu Wen-Tsun (1997)
Gerard Huet (1998)
Robert S. Boyer and J Strother Moore (1999)
William W. McCune (2000)
Donald W. Loveland (2001)
Mark E. Stickel (2002)
Peter B. Andrews (2003)
Harald Ganzinger (2004)
Martin Davis (2005)
Wolfgang Bibel (2006)
President of CADE Inc.
baader@tcs.inf.tu-dresden.de
Rustan Leino, Microsoft Research
Colin Stirling, University of Edinburgh
Ashish Tiwari, SRI International
CVF - Fourth International Workshop on Constraints in Formal Verification
DISPROVING - Workshop on Disproving: Non-Theorems, Non-Validity,
Non-Provability
ESARLT - Empirically Successful Automated Reasoning in Large Theories
(see the call in this newsletter)
ISABELLE-WS - Isabelle Workshop
LFMTP - International Workshop on Logical Frameworks and Meta-Languages:
Theory and Practice
VERIFY - 4th International Verification Workshop
Gail Pieper
pieper@mcs.anl.gov
January 2007