AARNEWS - February 2003



No. 58, February 2003


From the AAR President
Herbrand Award: Call for Nominations
Huet Elected to the Academie des Sciences
Call for Papers for Conferences

  • ESSLLI-2003 Student Session
  • Joint Conference CSL'03 and KGC
  • Fourth Panhellenic Logic Symposium
  • FTP'2003
  • PPDP 2003
  • LPAR'03
  • PDPAR'03
  • From the AAR President, Larry Wos...

    My congratulations to Gérard Huet for his election to the Academie des Sciences! That is indeed an honor. Please note that we welcome information of this kind for our AAR Newsletter.

    As I have occasionally done before, I am beginning the new year with a research challenge to AAR members. Specifically, from my various studies in logic and algebra, I have noticed that one is more likely to succeed in obtaining a proof if the axiom system has three or more axioms rather than a single axiom. The practical deductive power of a multiaxiom axiom system is greater than that of a single-axiom system. And this situation appears to be true regardless of whether one uses as a metric CPU time or length of proof or actual researcher's time or number of applications of a particular inference rule. Similarly, I have noticed that having a dependency in an axiom system gives that system more power, especially if the dependency is ``natural'' (for example, in group theory). The challenge then is the following. Establish the truth or falsity of the following conjecture: If one is working on an open question in logic or in algebra, one is more likely to succeed with a multiaxiom system than with a single axiom system and, similarly, one is more likely to succeed if the axiom system has dependencies.

    Herbrand Award:
    Call for Nominations

    Maria Paola Bonacina
    Secretary of AAR and CADE
    On behalf of the CADE Inc. Board of Trustees

    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)
    Woody Bledsoe (1994)
    Alan Robinson (1996)
    Wu Wen-Tsun (1997)
    Gérard Huet (1998)
    Robert S. Boyer and J Strother Moore (1999)
    William W. McCune (2000)
    Donald W. Loveland (2001)
    Mark E. Stickel (2002).

    A nomination is required for consideration for the Herbrand award. Nominations can be made at any time and remain open indefinitely, but only nominations received by

    1 April 2003
    will be considered for a Herbrand award at CADE in July-August 2003.

    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

    Ulrich Furbach
    President of CADE Inc.
    with copies to mariapaola.bonacina@univr.it.

    Herbrand Award Winner Gérard Huet Elected to the
    Academie des Sciences

    Maria Paola Bonacina
    (Secretary of AAR and CADE)
    E-mail: mariapaola.bonacina@univr.it

    I am happy to inform all members of the Association for Automated Reasoning that on November 19, 2002, AAR member and Herbrand award winner Gérard Huet of INRIA was elected to the French Académie des Sciences. I learned this good news from Claude Kirchner, also a member of our association.

    Gérard Huet received the Herbrand award in 1998, and the Herbrand award is listed prominently among his many honors in the article announcing his election on the INRIA site (see http://www.inria.fr).

    It is very important for the field of automated reasoning that members already recognized as leaders by our scientific community be elected to national academies, as such election represents an external recognition first and foremost to the individual, but also to the fields he chose to contribute to.

    Call for Papers

    ESSLLI-2003 Student Session

    The Student Session of the 15th European Summer School in Logic, Language and Information (ESSLLI-2003) will be held in Vienna, August 18-29, 2003.

    This eighth ESSLLI Student Session will provide an opportunity for ESSLLI student participants to present their work and get feedback from senior researchers and fellow students. The ESSLLI Student Session encourages submissions from students at any level, undergraduates (before completion of the master's thesis) as well as postgraduates (before completion of the Ph.D. degree). Papers co-authored by nonstudents will not be accepted. Papers may be accepted for full presentation (30 minutes, including 10 minutes of discussion) or for a poster presentation. All the accepted papers will be published in the ESSLLI-2003 Student Session proceedings, which will be made available during the summer school.

    The Student Session papers should describe original, unpublished work, completed or in progress, that demonstrates insight, creativity, and promise. Submissions are welcome within the areas of logic, language, and computation. Student authors should submit a full paper (up to 7 pages exclusive of references) by e-mail to b.ten.cate@hum.uva.nl by February 24, 2003.

    In order to present a paper at ESSLLI-2003 Student Session, at least one student author of each accepted paper has to register as a participant at ESSLLI-2003. The authors of accepted papers will be eligible for reduced registration fees even after the deadline for early registration.

    For all information concerning ESSLLI-2003, please consult the ESSLLI-2003 Web site. For more information concerning the ESSLLI-2003 Student Session, please consult the Web site. For other questions please send e-mail to Balder ten Cate (b.ten.cate@hum.uva.nl).

    Joint Conference CSL'03 and KGC

    The annual conference of the European Association for Computer Science Logic and the 8th Kurt Goedel Colloquium will take place in Vienna, August 25-30, 2003.

    Researchers are encouraged to submit articles on the following topics:

    The deadline for title and abstract is March 31, 2003, and the deadline for the full paper is April 7, 2003. For the required format of submissions see the Web site.

    A lecture, jointly invited by the CSL'03 & KGC and the European Summer Schiol in Logic Language and Information, will be given by Sergei Artemov (CUNY, USA). Additional lectures are being arranged. Several tutorials also are planned: verification of infinite state systems, computational epsilon calculus, quantifier elimination, and winning strategies and controller synthesis.

    Fourth Panhellenic Logic Symposium

    The 4th Panhellenic Logic Symposium will be held on July 7-10, 2003, in Thessaloniki, Greece. Original papers on all aspects of logic are solicited. Authors are invited to submit an extended abstract of at most five pages with a statement classifying the paper in one of the following areas: mathematical logic, set theory, logic in computer science, history of logic, philosophy of logic, or other logic-related areas (specified).

    Please submit the abstract to kirousis@ceid.upatras.gr by March 28, 2003. For further information, see the Web site.


    The 4th International Workshop on First-Order Theorem Proving, FTP'2003, will take place on June 12-14, 2003, in Valencia, Spain.

    The FTP workshop will focus on first-order theorem proving as a core theme of automated deduction and will provide a forum for presentation of recent work and discussion of research in progress. The workshop welcomes original contributions on the following:

    Authors are invited to submit papers in the following categories: (1) extended abstracts of 8-10 pages, describing original results not published elsewhere; (2) system descriptions of 3-5 pages, describing new systems or significant upgrades of existing ones, especially including experiments (systems will have to be freely available online); and (3) position papers of 2 pages, describing the authors' research interests in the field, work in progress, or future directions of research. Papers should be sent as a postscript or pdf file to ftp2003@uni-koblenz.de by April 1, 2003.

    Accepted submissions will be published in the ENTCS series (Electronic Notes in Theoretical Computer Science) and will be available electronically before the workshop.

    The workshop will be part of the Federated Conference on Rewriting, Deduction and Programming (RDP'03, http://www.dsic.upv.es/ rdp03/), together with RTA (the 14th International Conference on Rewriting Techniques and Applications), TLCA (the 6th International Conference on Typed Lambda Calculi and Applications), and several workshops.

    For regularly updated details of the workshop organization, visit the FTP'2003 Web page.
    For contacting the PC chairs: ftp2003@uni-koblenz.de.

    PPDP 2003

    The Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming will be held in Uppsala, Sweden, August 27-29, 2003.

    PPDP 2003 aims to stimulate research in the use of logical formalisms and methods for analyzing, specifying, and performing computations. Of general interest are all aspects surrounding declarative programming paradigms such as logic programming, functional logic programming, and constraint programming. Papers related to the use of declarative paradigms and tools in industry and education are especially solicited.

    Submissions must be made by March 29, 2003, and must be no more than 12 pages in standard ACM conference format. Details on formatting are available at the Web site..

    The proceedings will be published by ACM Press.

    PPDP 2003 is part of a federation meeting known as Principles, Logics and Implementations of high-level programming languages (PLI 2003), which includes the ACM SIGPLAN International Conference on Functional Programming (ICFP 2003). PLI will run August 25-29, 2003. The meetings will take place on the Uppsala University campus. Students who have a paper accepted for the conference are offered student membership in SIGPLAN free for one year; as members of SIGPLAN, they may apply for travel fellowships from the PAC fund.

    For further information, see the following Web sites:
    PPDP 2003
    PLI 2003

    Or, send e-mail to the conference chair Konstantinos Sagonas (kostis@it.uu.se).

    LPAR 2003

    The international conference on Logic for Programming Artificial Intelligence and Reasoning will take place September 22-26, 2003, in Almaty, Kazakhstan.

    Papers are solicited in the following areas:

    automated reasoning description logics
    interactive theorem proving nonmonotonic reasoning
    implementations of logic specification using logics
    design of logical frameworks logic in artificial intelligence
    program and system verification lambda and combinatory calculi
    model checking constructive logic and type theory
    rewriting computional interpretations of logic
    logic programming logical foundations of programming
    constraint programming logical aspects of concurrency
    logic and databases program extraction from proofs
    logic and computational complexity modal and temporal logics
    translation validation knowledge representation and reasoning
    proof-carrying code reasoning about actions
    logic in semantic web effectively presented structures
    proof planning  

    Both regular papers (15 pages) and experimental papers (10 pages) are welcome. The first category is intended to contain new results, the second one to describe implementations of systems, to report experiments with implemented systems, or to compare implemented systems. Abstracts are due April 28 and full papers May 5. The proceedings will be published by Springer-Verlag in the LNAI series and available at the conference.

    All questions related to submission should be sent to the program chairs: Moshe Y. Vardi (vardi@cs.rice.edu) and Andrei Voronkov (voronkov@cs.man.ac.uk). For further information, please see the Web site.


    A CADE-19 workshop on ``Pragmatics of Decision Procedures in Automated Reasoning'' (PDPAR'03) will be held in Miami, Florida, July 28-29, 2003. The main goal of this workshop is to bring together researchers interested in the pragmatical aspects of decision procedures in automated reasoning, giving them a forum for presenting and discussing implementation and evaluation techniques.

    Topics of interest include

    Another goal of the workshop is to provide a discussion forum for the SMT-LIB initiative, a research initiative aimed at establishing a common standard for the specification of benchmarks and background theories for satisfiability modulo theories, and at creating a repository of such benchmarks. (See the Web for more information.) The workshop will host panel discussions on the SMT-LIB format.

    Extended abstracts (up to 8 pages) addressing the pragmatical aspects of decision procedures are solicited. Submissions should be sent by email to pdpar03@cs.uiowa.edu by April 14, 2003. The authors of accepted submissions are expected to give a 25-minute presentation at the workshop. The proceedings of PDPAR'03 will be published as an INRIA technical report, and will be distributed at the workshop.

    Joint registration with the CADE-19 conference is possible but is not required. Refer to the CADE-19 Web site for registration instructions and deadlines: CADE-19.

    For further information, see the PDPAR'03 Web site.

    Gail W. Pieper
    February 2003