NEWSLETTER
From the AAR President
Announcement of CADE Elections
Abstract of Recent Ph.D. Thesis in AR
FMCAD 2006: Call for Participation
Logic Summer School
Call for Papers
From the AAR President, Larry Wos...
In reading the statements
from the four CADE candidates, I was struck by two items.
First is the repeated mention of the many smaller, and often competing,
subcommunities that have been spawned. I am delighted that automated reasoning
has expanded so greatly since the early 1980s. But, like the candidates, I am concerned that the field of automated reasoning itself
remains well recognized.
And this comment leads to my second point:
I note that CADE continues to receive high praise and
that each candidate not only believes automated reasonoing remains important
but has a clear vision about CADE's
role with IJCAR.
I encourage AAR members to read each candidate's statement carefully and take the time to vote.
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.:
The terms of Franz Baader, Peter Baumgartner, Uli Furbach, and Michael
Kohlhase are expiring. The position of Uli Furbach is taken by Frank
Pfenning as CADE-21 program chair. Thus, there are three positions to
fill.
The following candidates were nominated, and their statements are
below:
CADE is the major forum for discussing all aspects of automated
reasoning research (theory, implementation, and applications). While
theoretical work and work on implementations are very well represented
at CADE (through regular papers, system descriptions, and the system
competition), we must continue our work on attracting more papers on
applications, which are now often published at conferences related to
the application area (like CAV, KR).
In order to ensure the role of CADE as the flagship of automated
reasoning, we must try both to keep the high scientific standards of
the conference and to attract more automated reasoning-related
research from other areas (like knowledge representation, constraint
solving, verification, and computer algebra). Another important point
is to avoid a fragmentation of the field into many small and
specialized subcommunities with their own small conferences and
workshops. This does not mean that I am against having these smaller
events as well. But there should be one big event (every 2-3 years)
where the whole automated reasoning community meets and with which it
identifies. For this reason, I am strongly in favour of continuing the
IJCAR series and of CADE/IJCAR's participation in the FLoC
conferences.
As CADE president and head of the IJCAR steering committee, I have
tried to get more AR-related conferences involved in IJCAR (see,
e.g., the participation of TPHOLs in IJCAR'06) and would like to
continue these attempts in the future. I also think that our decision
to go into FLoC'06 as IJCAR rather than CADE was a good one since it
made IJCAR the second-largest conference (w.r.t. number of
participants) within FLoC. An important next step is to find a
schedule for IJCAR and FLoC that allows for a regular participation of
IJCAR within FLoC, while also keeping the identity of the IJCAR
constituent meetings, and in particular the role of CADE as the
flagship of automated reasoning research.
My research area is automated deduction, with a focus on automated
theorem proving in classical first-order logic and applications. CADE
is the main conference for me: I have attended CADE regularly since 1990,
co-authored several IJCAR or CADE papers, given a tutorial,
and co-organized several workshops at CADE, and our systems participate(d)
in CASC. I was the publicity chair of IJCAR in 2001, the workshop
chair of IJCAR 2004 and served on the programme committee of CADE and
IJCAR. I was the president of the FTP steering committee, and I am an
(outgoing) member of the Tableaux Steering committee. Since 2003 I have been
serving on the CADE board of trustees.
I think it is important to address the fragmentation of the field of
automated deduction. From the CADE perspective I am consequently very
much in favour of co-locating CADE with related conferences, having
CADE part of FLoC or integrating it into IJCAR on a regular basis. I
would like to see CADE to be more attractive for papers that are often
sent to KR, CAV or SAT but are within the scope of CADE, in particular
papers about applications of automated deduction technology in these
areas.
For more than a decade I have been an active and fascinated researcher in
automated deduction, and my first papers on extensional higher-order
theorem proving were presented at the 1998 CADE conference. I
consider symbolic reasoning and in particular automated deduction a
core challenge of AI, and I think that our field is currently not
appropriately positioned in the AI community. Automated deduction
plays an important role for proof (semi-)automation in modern proof
assistants and mathematics assistance systems (such as our OMEGA
system), and these systems in turn share many characteristics of large
AI systems in general. While the fragmentation of the research in AI
in the past decades, which was mirrored in the field of automated
deduction, had a very positive effect on the growing-up of its
subareas, I believe that the next decade should foster a mutual
fertilization and reintegration. I am glad to see that this process
has started. The scope of CADE has become wider over the last years,
and CADE is a driving force behind IJCAR.
Are the glory days of automated reasoning behind us? Have all the
interesting technical problems been solved, and all the worthwhile
application areas fully explored? Is the field doomed to a lingering
death by inches of incrementality and irrelevance?
You can count me in the ranks of those who say, absolutely not! I
believe that automated reasoning is crucial to the future of both
computer science and mathematics. When the Semantic Web is running
with description logic ontologies debugged using first-order provers,
then we can consider the work done. When proof assistants are
routinely used by mathematicians to develop their theories, and by
programming language designers to design, verify, and implement their
languages, then perhaps we can ponder the twilight of our field. And
until program verification based on a combination of manual proof and
automation is the industrial common practice, there are still plenty
of important problems to help drive both the practical and the
theoretical work of the field.
My own primary interest is in AR techniques for program verification.
As I have learned more about AR, I have been drawn to other subfields:
SMT solvers (I am a co-organizer of the annual Satisfiability Modulo
Theories Competition SMT-COMP, and a regular PC member of the SMT
workshop PDPAR), logical frameworks and type theory (CADE 2002 and
2003, JAR 2003), term rewriting and completion (RTA 2005 and 2006),
and most recently, proof assistants (I am applying Coq to reason about
programming language semantics). I served as a PC member for CADE
2005 and IJCAR 2006, and I am on the PC for RTA 2007.
To conclude, I believe automated reasoning has crucial contributions
still to make to computer science and mathematics. I ask for your
support for CADE trustee.
Author: Magnus Björk
Title: A First-Order Extension of Stålmarck's Method
Advisor: Mary Sheeran
Date of defence: May 11, 2006
Institution granting the degree: Department of Computer Science and Engineering, Chalmers
University of Technology, Gothenburg, Sweden
Abstract:
Stålmarck's method is an algorithm that decides validity of formulae in
propositional logic. It resembles many tableaux methods but uses a
special branch-and-merge-rule, called the dilemma rule. The dilemma
rule creates two branches, where a formula (called the dilemma
formula) is assumed to be false in one branch and true in the other one.
If neither of the branches turns out to be contradictory, then the
branches are merged into one branch again, retaining the common
consequences of the two branches.
We present a first-order version of Stålmarck's method. When branches are
merged in first-order logic, variables occurring in the respective
branches are unified, to retain as much information as possible. We show
that variables introduced in dilemma formulae must be treated rigidly in
the branches of the dilemma where they were introduced, but that they are
universal during and after the merge. Thus, the dilemma rule can be used
to introduce lemmas with universal variables.
We also present a proof procedure that searches for shallow dilemma
proofs. It begins by searching for proofs not including the dilemma rule,
then extends the search with non-nested dilemmas. After that, proofs with
at most two simultaneously open dilemmas are found, then with three, and
so on. The proof procedure does not substitute rigid variables
destructively; instead it explores an instance of the current dilemma,
after the branches have been merged. This is done to preserve as many
generalized conclusions as possible, and to be able to find new dilemma
formulae.
We show that the calculus and proof procedure are sound and complete. We
present encouraging benchmarks for the automated theorem prover Dilemma,
which is based on the method.
Author's correspondence address:
The
International Conference on Formal Methods in Computer-Aided Design
will take place
November 12-16, 2006, in San Jose, California
(note: ICCAD also takes place in San Jose the previous week, Nov. 5-9).
FMCAD 2006 is the sixth in a series of conferences on the theory and
applications of formal methods in hardware and system verification. FMCAD
provides a leading forum to researchers in academia and industry for
presenting and discussing groundbreaking methods, technologies,
theoretical results, and tools for reasoning formally about computing
systems. In addition to the technical program, FMCAD will offer a full
day of tutorials:
FMCAD will also include
a panel on complementing simulation with formal methods and an affiliated
workshop on pre- and postsilicon verification.
The early registration deadline is October 22, 2006.
For more information, see the
Web site.
The Logic Summer School at
the Australian National University (ANU), to be held December 4-14, 2006,
will comprise a blend of practical and theoretical
short courses on aspects of pure and applied logic taught by
international and national experts. The school provides a unique
learning experience for all participants, backed up with
state-of-the-art computational science facilities at the ANU.
Completeness theorems
Model theory and proof theory
Automatic deduction
Logic-based planning and diagnosis
Belief revision and nonmonotonic logics
Description logics
The summer school is intended for
(1) students from about the third year of undergraduate studies up to
beginning Ph.D. level who are considering specializing in a
logic-related field;
(2) teachers who teach logic in computer science, mathematics, or
philosophy; (3)
IT professionals who use formal methods or who want to know more about
logic-based technology; and (4)
anyone who finds the idea of two weeks of wall-to-wall logic enticing!
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.
Registrations after Friday, 27 October 2006, are subject to a 20%
surcharge.
To register or for more information visit the
Web site.
The 18th International Conference on Rewriting Techniques and Applications
(RTA'07) will take place in Paris, France, June 26-28, 2007.
RTA-07 is organized as part of the Federated Conference on Rewriting,
Deduction, and Programming (RDP'07), which comprises, in addition to RTA'07,
the conference on Typed Lambda Calculi and Applications (TLCA'07) and eight
workshops (HOR, PATE, RULE, SecReT, UNIF, WFLP, WRS, and WST).
RTA is the major forum for the presentation of research on all aspects of
rewriting. Typical areas of interest include
Best Paper Award:
An award is given to the best paper or papers as decided
by the program committee.
Submissions:
Submission categories include regular research papers and system descriptions.
Problem sets and submissions describing interesting applications of rewriting
techniques are also welcome. The page limit for submissions is 15 pages in
Springer LNCS style (10 pages for system descriptions). The submission Web
page will be made available beginning of December. As usual, the proceedings
of RTA'07 will be published in the Springer LNCS series.
The deadline for electronic submission of title and abstract
is Jan. 26, 2007; the deadline for electronic submission of papers
is Jan. 31, 2007.
Please consult the RTA'07 conference
Web page
for further information.
CiE 2007
The Third Conference CiE 2007, organized by CiE (Computability in
Europe) will take place at the University of Siena, June 18-23 2007.
CiE is a European network of mathematicians, logicians, computer scientists,
philosophers, theoretical physicists and others interested in new developments
in computability and in their underlying significance for the real world.
CiE 2007 will address various aspects of the ways computability and
theoretical computer science enable scientists and philosophers to deal
with mathematical and real-world issues, ranging through problems
related to logic, mathematics, physical processes, computation, and
learning theory. At the same time it will focus on different ways in
which computability emerges from the real world, and how this affects
our way of thinking about everyday computational issues.
Topics include artificial intelligence,
formal methods, and
uncertain reasoning.
CiE 2007 will be colocated with the annual CCA (Computability and Complexity
in Analysis) Conference June 16-18, 2007.
Papers (max. 10 pages) are due Jan. 12, 2007.
The conference proceedings will be published by LNCS, Springer Verlag. There
will also be journal special issues, collecting invited contributions related
to the conference.
For further information, see the
Web page.
LICS 2007
The 22nd
annual IEEE Symposium on Logic in Computer Science
will take place on
July 10-14, 2007, in Wroclaw, Poland,
colocated with ICALP 2007 and Logic Colloquium 2007.
Topics include
automated deduction, categorical models and logics,
concurrency and distributed computation, constraint programming,
formal methods,
lambda and combinatory calculi, linear logic,
logics in artificial
intelligence, modal and
temporal logics,
reasoning about security,
rewriting,
and verification.
Abstracts are due Jan. 15, 2007, with full papers due Jan. 22, 2007.
For details, see the
Web site.
LICS Workshops
Workshops are planned
for July 8, 9 and July 15 (possibly the afternoon of 14th).
LICS workshops have traditionally been an important and exciting part of
the program. They introduce either newest research in traditional areas of
the LICS community, recent interdisciplinary and applied areas of general
theory, or emerging directions that already have some substantial overlap
with LICS community interests. Researchers and practitioners are invited to
submit proposals for workshops on topics relating logic - broadly construed - tocomputer science or related fields. Typically, LICS workshops feature a
mix of invited speakers and contributed presentations. LICS workshops do not
produce formal proceedings. However, in the past there have been special issues of
journals based in part on certain LICS workshops.
Proposals should include the following:
Proposals are due Nov. 15, 2006, and should be submitted electronically to
Philip Scott, Workshops Chair, LICS 2007,
phil@site.uottawa.ca.
WoLLIC'2007
The 14th Workshop on Logic, Language, Information and Computation
will take place in
Rio de Janeiro, Brazil,
July 2-5, 2007.
WoLLIC is an annual international forum on interdisciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning.
Contributions (10 pages) are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive
areas of interest are foundations of computing and programming;
novel computation models and paradigms; broad notions of proof and belief;
formal methods in software and hardware development; logical approach to
natural language and reasoning; logics of programs, actions and resources;
and foundational aspects of information organization, search, flow, sharing,
and protection.
Papers must be submitted electronically on the
Web.
A title and single-paragraph abstract should be submitted by
February 23, 2007, with the full paper due March 2, 2007.
Proceedings, including both invited and contributed papers,
will be published in advance of the meeting.
ASL sponsorship of WoLLIC'2007 will permit ASL student members to
apply for a modest travel grant (deadline: April 1, 2007).
See www.aslonline.org/studenttravelawards.html for details.
TABLEAUX 2007
TABLEAUX 2007 -
Automated Reasoning with
Analytic Tableaux and Related Methods - will take place 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 all aspects--theoretical foundations, implementation techniques, systems development and applications--of the mechanization of reasoning with tableaux and related methods.
One or more tutorials will be part of the conference program.
For further information, see the
Web site.
SMT
The Journal on Satisfiability, Boolean Modeling and Computation
will publish a
special issue on satisfiability modulo theories.
SMT is the problem of deciding the
satisfiability of first-order formulas with respect to some
decidable background theory (e.g., linear arithmetic, the theory of
arrays, the theory of bit-vectors).
SMT techniques are gaining increasing relevance in many application
domains, including formal verification of hardware and software,
compiler optimization, planning and scheduling.
SMT is strongly related to SAT, as most SMT tools are built on top of
or interface with efficient SAT solvers.
Topics of interest for this special issue include
novel general SMT techniques,
novel SMT techniques for theories of interest,
SMT for combined theories,
novel implementation techniques for SMT, and
applications of SMT.
Submissions should be written in LaTeX and formatted according to JSAT's
author guidelines, and should not exceed 20 pages.
The deadline for paper submission (provisional) is November 25, 2006.
The guest editors are
Byron Cook (Microsoft Research - bycook@microsoft.com)
and
Roberto Sebastiani (DIT, Università di Trento - rseba@dit.unitn.it).
For further information visit the
Web page,
or send an email to one of the guest editors.
Computer Security: Foundations and Automated Reasoning
In connection with the Joint Workshop on
Foundations of Computer Security
and
Automated Reasoning for Security Protocol Analysis
(FCS-ARSPA'06),
a satellite event of LICS'06 as part of FLoC 2006,
a special issue of Information and Computation will be devoted to original
papers on foundations and formal methods in computer security.
Contributions are welcomed on the following topics and related ones:
Authors should submit an abstract by Nov. 5, 2006.
Full papers should be submitted electronically by Nov. 12, 2006, in portable
document format (pdf) or postscript (ps), by sending an email with
subject ``I&C submission'' to the address
fcs-arspa06@lists.inf.ethz.ch
with the file of the paper as an attachment.
The guest editors are
Pierpaolo Degano (Università di Pisa, Italy),
Ralf Kuesters (ETH Zurich, Switzerland),
Luca Vigano (ETH Zurich, Switzerland),
and Steve Zdancewic (University of Pennsylvania, USA).
For further information, see the
Web site.
Amy Felty
(Secretary of AAR and CADE)
E-mail: afelty@site.uottawa.ca
David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)
Peter Baumgartner (elected 10/2003)
Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)
Amy Felty (Secretary, appointed 5/2004)
Uli Furbach (IJCAR 2006 Program Co-chair)
Rajeev Goré (elected 10/2004)
Reiner Haehnle (Vice President, elected 10/2005)
Michael Kohlhase (elected 10/2000, reelected 10/2003)
Neil Murray (Treasurer)
Frank Pfenning (CADE-21 Program Chair)
Geoff Sutcliffe (elected 10/2004)
Cesare Tinelli (elected 10/2005)
Statement by Franz Baader
Statement by Peter Baumgartner
Statement by Chris Benzmueller
Statement by Aaron Stump
E-mail: mab@cs.chalmers.se
The Australian National University
Program Topics
Gail Pieper
pieper@mcs.anl.gov
October 2006