NEWSLETTER
No. 80, March 2008
From the AAR President
ProofBuilder: A Versatile Interactive Prover for Beginning Students
Workshops
From the AAR President, Larry Wos...
Since I am not a traveling man but have, like most of the world, gotten involved with the Internet, I recently noted that the Wikipedia article on automated reasoning could use an update.
Certainly, I do not consider the area a "subfield of artificial intelligence" -- though perhaps AAR readers do, in which case we could launch an interesting debate.
ProofBuilder runs straightforwardly on all platforms with Java;
it allows users to copy/paste formulas from Web pages, MS Word, PDF, and so forth;
it adapts to the symbols that users enter for "implies," "forall," and the like;
and it supports many proof styles including
transforming expressions according to logical equivalences or equations or
comparisons ("<", ">", etc.),
direct proof, backward chaining,
handling subcases separately,
nonclausal resolution,
proof by example or counterexample,
stepwise and strong induction,
and
proof by contradiction.
This prover can handle the material of an introductory course or textbook
on Discrete Mathematics, including propositions, quantifiers, sets,
summations,
O(), divisors, modulus, and combinatorics.
The author of ProofBuilder is Hugh McGuire,
from Grand Valley State University, MI, U.S.A.
For further information, see the documentation with examples on the
Web.
Workshop on Automated Reasoning
ARW will take place July 30-31, 2008, at the University of Birmingham.
Titled "Bridging the Gap between Theory and Practice," this
workshop continues the series workshops and will provide an informal forum for the automated reasoning community to discuss recent work, new ideas and current trends. It aims to bring together researchers from all areas of automated reasoning in order to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines; among researchers from academia, industry and government; and between theoreticians and practitioners.
The series covers the full breadth and diversity of automated reasoning, including topics such as logic and functional programming; equational reasoning; deductive databases; unification and constraint solving; the application of formal methods to specifying, deriving, transforming and verifying computer systems and requirements; deductive and non-deductive reasoning, including abduction, induction, nonmonotonic reasoning, and analogical reasoning; commonsense reasoning; and the wide range of topics that fall under the heading of knowledge representation and reasoning.
The workshops in this series are highly interactive, giving all attendees the opportunity to participate. The workshops contain many open discussion sessions organized around specific topics, and often contain sessions for displaying posters and presenting system demonstrations. This is intended to be an inclusive workshop, with participants encouraged from the broad spectrum covered by the field of automated reasoning. We encourage the participation of experienced researchers as well as those new to the field, especially students.
For more details see the ARW 2008
Web site.
PAAR-2008
The first workshop on Practical Aspects of Automated Reasoning
will be held August 10 or 11, 2008, in Sydney, Australia. PAAR will be
associated with the 4th International Joint Conference on
Automated Reasoning (IJCAR-2008).
PAAR provides a forum for developers of automated reasoning
tools to discuss and compare different implementation
techniques, and for users to discuss and communicate their
applications and requirements. This workshop will bring
together different groups to concentrate on practical aspects
of the implementation and application of automated reasoning
tools. It will allow researchers to present their work in
progress, and to discuss new implementation techniques and
applications.
Topics include
the following:
We are particularly interested in contributions that help the
community to understand how to build useful and powerful
reasoning systems in practice, and how to apply existing
systems to real problems.
Researchers interested in participating are invited to submit a
short (2-10 pages) abstract via EasyChair. Submissions will be
refereed by the program committee, which will select a balanced
program of high-quality contributions.
Submissions should be in standard-conforming Postscript or PDF.
To submit a paper, go to the
EasyChair PAAR page
and follow the instructions there.
The final versions should be prepared in LaTeX using the
Springer Verlag llncs class. The workshop proceedings will be
published as a technical report and distributed at the event.
If quality and quantity of the subissions warrants this, we
plan to produce a special issue of a recognized journal on the
topic of the workshop.
Abstracts are due May 27, 2008;
camera-ready versions due: July 7th, 2008
For further information, please see the
Web site.
VERIFY 2008
The 5th International Verification Workshop
(VERIFY 2008) will be held in Sydney, Australia,
August 10-11.
The VERIFY workshop series brings together people interested
in the development of safety and security critical systems, in formal methods,
in the development of automated theorem proving techniques, and in the
development of tool support. Practical experiences gained in realistic
verifications are of interest to the automated theorem proving community and
new theorem-proving techniques should be transferred into practice. The
overall objective of the VERIFY workshops is to identify open problems and to
discuss possible solutions under the theme
What are the verification problems? and What are the deduction techniques?
The scope of VERIFY includes topics such as the following:
CEDAR'08
The goal of CEDAR is to bring together researchers interested in problems that are in the interface between automated reasoning and computational complexity, in particular in the following:
Topics of interest for CEDAR 2008 include
the following:
We plan to accept three types of papers:
Given the informal style of the workshop, the submission of papers presenting student's work and work in progress is encouraged. Submission of papers is via
Easychair.
The final versions of the selected contributions will be collected in a volume to be distributed at the workshop. These informal proceedings will also be made accessible on the web.
A special journal issue is planned.
For further information, see the
Web site.
First-order theorem proving is one of the core themes of automated deduction and one of its most mature subfields. First-order logic is sufficiently expressive to allow the specification of a wide range of problems in a natural way. At the same time an extensive variety of sound and complete calculi for first-order logic exists which have been implemented in a number of high-quality, fully automated reasoning systems. These in turn make it not only possible to effectively solve problems formulated in first-order logic, but also make it attractive to consider closely related logics, for example, many-valued, description, and modal logics, from a first-order perspective.
This special issue is intended to present recent advances in the field to an audience of applied logicians, automated deduction theorists and applications specialists.
This special issue will focus on first-order theorem proving as a core theme of automated deduction, in particular:
The deadline for submissions is May 28, 2008. For further details see the
Web page.
JELIA 2008
The
11th European Conference on Logics in Artificial Intelligence
will take place
September 28 to October 1, 2008, in Dresden, Germany.
JELIA 2008 strives to foster links and facilitate
cross-fertilization of ideas between researchers from various
disciplines, between researchers from academia and industry, and
between theoreticians and practitioners.
Authors are invited to submit papers presenting original and
unpublished research in all areas related to the use of logics in AI.
Topics of interest include the following:
Further information about JELIA 2008 is available at
the
Web site.
Rewriting Techniques and Applications
The 19th International Conference on Rewriting Techniques and
Applications (RTA 2008)
will be held on July 15-17, 2008, at the
Castle of Hagenberg, Austria.
The conference
is organized as part of the RISC Summer
2008, which comprises five conferences, five workshops and the
Training School in Symbolic Computation, and is followed by the
3rd International School on Rewriting in Obergurgl.
RTA is the major forum for the presentation of research on all
aspects of rewriting. Typical areas of interest include the following:
Submission categories include regular research papers
(15 pages) and system descriptions (10 pages).
Problem sets and submissions describing
interesting applications of rewriting techniques are also welcome.
Papers must be submitted
electronically through the
EasyChair system,
An award will be given to the best paper or papers as decided by the
program committee.
Limited student support will be available and announced in future
versions of this call.
For further information, see the
Web page.
MICAI 2008
The 7th Mexican International Conference on
Artificial Intelligence will take place in Mexico City, Mexico,
October 27-31, 2008.
Topics of interest include all areas of artificial intelligence. Poster
session, workshops, tutorials, and cultural events are planned.
Papers accepted for oral session will be published by Springer in LNAI:
Lecture Notes in Artificial Intelligence. Poster session papers will
be published separately. Special issues of journals are anticipated.
Submissions are received via the
Web.
Abstracts are due May 5, full text by May 12.
General inquiries should be sent to micai2008 at MICAI.org.
IMLA'08
The Fourth International Workshop on
Intuitionistic Modal Logic and Applications
(IMLA'08)
will take place in
Pittsburgh, Pennsylvania, June 23, 2008.
Constructive modal logics and type theories are of increasing foundational and practical relevance in computer science. Applications are in type disciplines for programming languages, and meta-logics for reasoning about a variety of computational phenomena.
Theoretical and methodological issues center around the question of how the proof-theoretic strengths of constructive logics can best be combined with the model-theoretic strengths of modal logics. Practical issues center around the question which modal connectives with associated laws or proof rules capture computational phenomena accurately and at the right level of abstraction.
This workshop will bring together designers, implementers, and users to discuss all aspects of intuitionistic modal logics and type theories.
Topics include the following:
We solicit submissions on work in progress and on more mature results. Submissions should be extended abstracts of 5-10 pages sent in
PostScript or PDF format to the program co-chair at aleksn@microsoft.com.
Submissions are due April 25, 2008.
We plan to publish the workshop proceedings as Electronic Notes in Theoretical Computer Science (ENTCS) or in CEURS, to be decided.
Authors should use the generic
ENTCS macro package.
For further information, see the
Web page.
AiML-2008
Advances in Modal Logic will take place at LORIA in Nancy, France,
September 9-12, 2008.
http://aiml08.loria.fr
AiML is an initiative aimed at presenting
an up-to-date picture of the state of the art in modal logic
and its many applications. The initiative consists of a
conference series together with volumes based on the conferences.
Authors are invited to submit on all aspects of modal logics, including
the following:
In a change from previous AiML's, there will be two types of paper:
full papers for publication and presentation at the conference, and
abstracts for short presentation only.
Both types of paper should be submitted electronically using the
submission
page.
The online submission system will be opened a few weeks before the
submission deadline of March 31, 2008.
Full papers (max. 15 pages) will be published by
College Publications in a volume to be made available at the meeting.
Abstracts should at most 5 pages. They may describe preliminary
results, work in progress, and so forth and will be subject to light review.
They may be made available at the conference, and authors should
indicate if they would like to make a short presentation of their
abstract of up to 15 minutes.
The summer academy at TU Dresden will focus on the long-lasting controversy of
the relationship between modern formal logic (including its use for
automated reasoning and computation) and the
rationality and common sense underlying human reasoning.
Traditionally, a huge gap is perceived between the symbolic
representation of knowledge used in modern logic and the
subsymbolic representation considered dominant in human reasoning.
Psychological experiments even suggested that people
often don't reason logically and, in general, that logic seems to
play only a minor role in human reasoning. However, recently, new
ways of explaining human reasoning seem to revive its relatedness to
logic. For this reason this summer academy seeks to bring
together researchers from both sides for an exchange of views.
The participation fee is 200 EUR.
A limited number of grants may be available.
Applicants should indicate in the application if
a grant is essential for participation.
Applications for grants must
include an estimate of travel costs (to be filled in the
respective part of the online registration form).
Participants must register by April 1, 2008
(see the online registration on the
Web page).
For those who want to apply for a grant, this deadline is
obligatory.
After April 1, 2008, registration will be possible as
long as there are vacant places.
People applying until April 1, 2008, and applying for a
grant will be informed about respective decisions on
grants at the latest by the end of April.
It will be possible for some participants to present
their research work during a small workshop integrated in
the summer school.
Those wishing to do so should
register by means of the online workshop registration
form on the web page (the title of the
proposed talk, and, in addition, an extended abstract or
a full paper of at most 10 pages in postscript or pdf
format must be submitted by April 1, 2008).
Participation at the summer school is a
prerequisite for participation at the workshop.
The course program is as follows:
If I were a traveling man, I would say this summer would be an ideal time to travel the world -- from Pennsylvania to Austria to Australia -- participating in several exciting conferences and workshops on automated reasoning.
I am particularly intrigued by the new workshop titled PAAR, which appears to emphasize the application of reasoning programs to real problems. While I am interested in theory, the way one can truly measure the success of automated reasoning is in the number, variety, and type of problem that can be solved.
Special Issue on First-Order Theorem Proving
Guest Editors: Silvio Ranise and Ullrich Hustadt
Technische Universitaet Dresden
August 24 - September 6, 2008