AARNEWS - September 2003



No. 60, September 2003

From the AAR President
Call for Papers

  • FLOPS 2004
  • IJCAR 2004
  • Call for Workshop Proposals
    Announcement of CADE Elections
    Call for Journal Submissions

    From the AAR President, Larry Wos...

    CADE has an important election coming. Several of the candidates discuss the importance of strengthening CADE and their concern about having CADE (and automated reasoning researchers) place more emphasis on applications. I encourage you to read the statements of the nominees carefully and then vote when you receive your ballot.

    Call for Papers

    FLOPS 2004

    The Seventh International Symposium on Functional and Logic Programming will take place in Nara, Japan, on April 7-9, 2004. The symposium is a forum for research on all issues concerning functional programming and logic programming. In particular, it seeks to stimulate the cross-fertilization as well as integration of the two paradigms. The symposium takes place about every 1.5 years in Japan.

    Masami Hagiya (University of Tokyo), Carsten Schuermann (Yale University), and Peter Selinger (University of Ottawa) will give invited presentations.

    Submitted papers should be one of two types: (1) regular research papers that describe new results, or (2) system descriptions, containing a link to a working system. All submissions must be written in English and can be up to 15 proceedings pages long. Authors are strongly encouraged to use LaTeX2e and the Springer llncs class file. The submission deadline is October 1, 2003.

    For further information, see the Web site.

    IJCAR 2004

    The Second International Joint Conference on Automated Reasoning (IJCAR) is the fusion of several major conferences in automated reasoning:

    These five events will join for the first time at the IJCAR conference in Cork in July 2004.

    IJCAR 2004 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.

    Logics of interest include the following: propositional, first-order, classical, equational, higher-order, nonclassical, constructive, modal, temporal, many-valued, substructural, description, metalogics, type theory, and set theory.

    Methods of interest include the following: tableaux, sequent calculi, resolution, model-elimination, connection method, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, efficient datastructures and indexing, integration of computer algebra systems and automated theorem provers, and combination of logics or decision procedures.

    Applications of interest include the following: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, natural language processing, linguistics, robotics, and planning.

    Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Research papers can be up to 15 proceedings pages long, and system descriptions can be up to 5 pages long. The proceedings of IJCAR 2004 will be published by Springer-Verlag in the LNAI/LNCS series.

    For details, see the Web site.

    Important Dates

    January 5, 2004: Submission deadline
    March 22, 2004: Notification of acceptance
    April 14, 2004: Camera-ready copy due
    July 4-8, 2004: IJCAR 2004

    Best Paper Awards

    A prize of 300 Euros will be given to the best paper. In addition, a prize of 300 Euros will be given to the best paper written solely by one or more full-time students (at the time of submission). Students must indicate with their submission that they would like their paper to be considered for this award. The program committee may decline to make the awards or may split it among several papers.

    Full information on IJCAR may be found at the Web site.

    Call for Workshop Proposals

    IJCAR workshops will be held on July 4 and July 5, 2004. They will run for one or two days, but half-day ones are possible as well. Workshop proposals are solicited on IJCAR-related topics as mentioned previously in the Call for Papers. Particularly welcome are proposals that promise to bring new topics into IJCAR, of either practical or theoretical importance, or provide a forum for more detailed discussion on central topics of continuing importance. Workshops that close the gap between automated reasoning and related areas, for instance formal methods or software engineering, are especially encouraged.

    Each workshop must have one or more designated organizers and may have a program committee as well. Workshop proposals must be limited to three pages and provide at least the following information:

    Workshop proposals should be sent as plain text and as postscript or PDF to the workshop chair (peter@uni-koblenz.de) no later than November 16, 2003.

    Workshop organizers are expected to maintain a Web site showing all the relevant information of their workshop, including online versions of accepted papers. Workshop organizers are responsible on their own for sufficient distribution of their call for papers and other publicity (general IJCAR announcements will mention the IJCAR workshops as well). The IJCAR organizers offer to copy and distribute the workshop notes to registered workshop participants.

    In case of questions or problems, please contact the workshop chair:

    Peter Baumgartner
    Tel. +49 261 287-2777
    Web site

    Important Dates:

    Deadline for proposal submissions: 16 November 2003
    Acceptance/rejection notification: 12 December 2003
    Deadline for camera-ready copy of workshop notes: 13 June 2004
    Workshop date: 04 July 2004 - 05 July 2004

    Announcement of CADE Elections

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

    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.:

    Franz Baader (CADE 2003 Program Chair: term expired)

    David Basin (IJCAR 2004 Program Co-chair)

    Maria Paola Bonacina (Secretary)

    Gilles Dowek (elected 9/2001)

    Ulrich Furbach, President (elected 8/1997 and 10/2000: term expired)

    Harald Ganzinger (past Program Chair, elected 10/1999 and 10/2002)

    John R. Harrison (elected 9/2001)

    Michael Kohlhase (elected 10/2000: term expired)

    David McAllester (past Program Chair, elected 10/2000: term expired)

    Neil V. Murray (Treasurer)

    Frank Pfenning, Vice-President (elected 10/1998 and re-elected 9/2001)

    Andrei Voronkov (past Program Chair, elected 10/2002)

    Toby Walsh (elected 10/2002)

    The terms of office of Franz Baader, Ulrich Furbach, Michael Kohlhase and David McAllester are expiring. The position of Franz Baader is taken by David Basin, as IJCAR 2004 program co-chair. Thus, there are three positions to fill, to replace the three trustees that were elected in October 2000, since CADE trustees are elected to serve for three years.

    The following candidates were nominated:

    Franz Baader nominated by Harald Ganzinger and Michael Kohlhase

    Peter Baumgartner nominated by Ulrich Furbach and Mark Stickel

    Michael Kohlhase nominated by Alan Bundy and Toby Walsh

    Stephan Schulz nominated by Geoff Sutcliffe and Tanel Tammet

    and provided the following statements.

    Statement by Franz Baader

    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 well represented at CADE (through regular papers, system descriptions, and the system competition), we must still work on attracting more work on applications, which are now more often published at conferences related to the application area.

    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's participation in the FLoC conferences. In order to give CADE more weight within FLoC, it might be a good idea to combine both, i.e., automated reasoning events should rather participate as IJCAR than as separate events in FLoC.

    Statement by Peter Baumgartner

    My main research area is automated deduction, with focus on classical first-order logic. In the first place I investigate tableau and Davis-Putnam-like calculi, and I am particularly interested in implementations and their practical applications.

    I attend the CADE conferences regularly since 1990, served on the programme committee, was the publicity chair in 2001 (when CADE joined IJCAR) and I am the workshop chair of IJCAR 2004. Currently, I am the president of the FTP (First-Order Theorem Proving workshops) steering committee.

    Concerning the field of Automated Deduction, I feel it is important not only to pursue theoretical research, but also to actively pick-up significant real-world problems and apply automated deduction technology for solving them. This should also help to achieve higher awareness of our field on a broader scope. Related to CADE, the last CADEs did not see too many papers on technology with a high potential for practical applications, such as SAT techniques or description logics. I think it is important to raise CADE's attractivity in this direction. I am also very much in favour of co-locating CADE with related conferences, making CADE part of FLoC or integrating it into IJCAR.

    I feel very pleased to be nominated for the CADE steering committee!

    Statement by Michael Kohlhase

    I consider CADE my home community, and I am therefore concerned about its state and direction. If I am re-elected CADE trustee, I would like to make CADE more OPEN (to researchers from neighboring fields) APPLIED (to real-world problems not just introspective challenge examples), and INTEGRATED (the IJCAR effort must be stabilized and strengthened). With more progress on these, keeping up the high academic standards of the CADE conference, I believe that CADE can look towards a healthy future. Not all of these objectives can be reached by the trustees alone, but their actions can lead the CADE community into the right direction. I personally can help with the first two issues, due to my close ties to the computational linguistics and mathematics communities. I would also act as a liaison person with the QPQ initiative (see the AAR newsletter for June 2003). Please see my full statement on the Web.

    Statement by Stephan Schulz

    I started working in the field of automated deduction as a student in 1993. From 1995 to early 2003 I was a member of the Automated Reasoning Group at TU Munich. I taught computer science at the University of Miami for one term in 2002, and currently am a CALCULEMUS researcher, associated with RISC-Linz. In addition to academic work, I have also worked as a consultant on first-order reasoning for Safelogic A.B. in Gothenburg, Sweden. My main research interests are proof search and presentation, efficient and robust implementations, and machine learning. I'm probably best known as the author of the equational theorem prover E. Depending on your view, I've been a member of the CADE community since 1994, when my very first submission was rejected, or 1996, when I presented a paper at CADE-13 in New Brunswick. You can find out more about me and my work at my Web site.

    CADE is the core conference for the automated deduction community. In order to maintain this position and to serve as the focus of research in automated reasoning, it should strive to maintain a balance between theoretical, practical and applied research. In particular, I think CADE should try to attract more papers about implementing deduction systems in real-world settings, and bridging the gap between theoretical results and practical applicability. To achieve this, every CADE program comittee should be a representative sample of deduction researchers, with members from all major fields. In my opinion, the current rhythm of CADE, IJCAR, and FLoC/CADE works very well, on the one hand allowing the different deduction conferences to maintain their identities and different foci, while on the other hand supporting cross-fertilization and a single community.

    Call for Journal Submissions

    Special JAR Issue: First-Order Theorem Proving

    Following the tradition of the previous workshops on first-order theorem proving, a special issue will be edited to commemorate the fourth workshop in this series. This special issue will be published by Kluwer Academic Publishers within the Journal of Automated Reasoning.

    This special issue will focus on first-order theorem proving as a core theme of automated deduction, including

    This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals or refereed conferences. The contributions are not limited to those presented at the workshop FTP'2003.

    Editors of this special issue:

    Ingo Dahn, Universitaet Koblenz-Landau
    Deepak Kapur, University of New Mexico
    Laurent Vigneron, LORIA - Universite Nancy 2

    To submit a paper, send a Postscript or PDF file to ftp2003@uni-koblenz.de. Papers will be refereed following the standard JAR reviewing process.

    Important Dates:

    Paper submissions: October 15, 2003
    Notification of acceptance: February 16, 2004
    Publication: by the end of 2004

    For further information, see the Web page or the more general page on FTP in 2003. If you have further questions, send to ftp2003@uni-koblenz.de.

    Gail Pieper Technical editor September 2003