AARNEWS - June 2003

ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 59, June 2003

From the AAR President
Announcement of the 2003 Herbrand Award
Call for Nominations: CADE Trustees Election
Call for Submissions

  • ICLP'03
  • ICoS-4
  • New Book
    Call for Contributions: QPQ Deductive Software Repository
    Open Question

    From the AAR President, Larry Wos...

    I hail the efforts of Mark Stickel in establishing an open source repository for deductive software. Having a variety of tools and libraries available will, I hope, encourage researchers to experiment with different systems and procedures, perhaps using the benchmark suites that are also provided. I strongly encourage AAR members to visit this new site.

    I also encourage researchers to attack the open question in combinatory logic presented at the end of this newsletter. If you succeed in finding an answer, I would be most delighted to hear from you.



    Announcement of the 2003 Herbrand Award

    Peter B. Andrews will be awarded the Herbrand Award at CADE 2003 for his seminal contributions and pioneering research in type theory, mating-based theorem proving, automated deduction in higher-order logic, logic education, and many other contributions to the field of automated reasoning.

    Call for Nominations: CADE Trustees Election

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

    Nominations for three CADE trustee positions are being sought, in preparation for the elections to be held next fall.

    Nominations can be made by any AAR member, either by e-mail or in person at the CADE 2003 business meeting. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be or be willing to become AAR members. For further details please see the CADE Inc. bylaws at the Web site.

    The board of trustees currently includes (in alphabetical order):

    Franz Baader, CADE 2003 program chair, Germany
    David Basin, IJCAR 2004 program co-chair, Switzerland
    Maria Paola Bonacina, Secretary, Italy
    Gilles Dowek, elected 9/2001, France
    Ulrich Furbach, President, elected 8/1997 and 10/2000, Germany
    Harald Ganzinger, former program chair, elected 10/1999 and 10/2002, Germany
    John R. Harrison, elected 9/2001, U.S.A.
    Michael Kohlhase, elected 10/2000, U.S.A.
    David McAllester, former program chair, elected 10/2000, U.S.A.
    Neil V. Murray, Treasurer, U.S.A.
    Frank Pfenning, Vice-President, elected 10/1998 and 9/2001, U.S.A.
    Andrei Voronkov, former program chair, elected 10/2002, U.K.
    Toby Walsh, elected 10/2002, Ireland

    The terms of Ulrich Furbach, Michael Kohlhase and David McAllester expire after CADE 2003, because CADE Trustees are elected for three years. The term of office of Franz Baader also expires with CADE 2003, but his position is taken by David Basin as IJCAR 2004 program co-chair. Thus, there are three trustees to elect (the IJCAR 2004 program co-chairs are David Basin and Michael Rusinowitch; the CADE trustees offered them to serve on the board, and they agreed that David will).

    Among the outgoing trustees, Michael Kohlhase and David McAllester are eligible to be nominated for a second term, and Franz Baader is eligible to be nominated for a first term as elected trustee; Ulrich Furbach is not eligible because one cannot be elected for three consecutive terms.

    E-mail nominations are to be sent to CADE-board@sci.univr.it before the end of CADE (August 2, 2003).

    Call for Submissions

    ICLP'03

    The International Conference on Logic Programming 2003 will be held in Mumbai (Bombay), India, December 9-13, 2003 (in conjunction with FSTTCS'03 and ASIAN'03).

    Posters are sought in all areas of logic programming:

    Posters provide an excellent forum for presenting late-breaking or speculative work in an interactive and informal setting. Submission details for papers and posters can be found on the conference Web page. Submission deadline is June 28, 2003.

    ICoS-4

    The fourth workshop on Inference in Computational Semantics will take place in Nancy, France, September 25-26, 2003. It will be part of a special Nancy Inference Week: on the day before ICoS-4 (24 September) there will be a one-day school on description logic and its applications in linguistics, and on the two days preceding that (September 22-23, 2003) the third Method for Modalities (M4M-3) workshop will be held.

    Traditional inference tools (such as theorem provers and model builders) are reaching new levels of sophistication and are now widely and easily available. A wide variety of new tools (statistical and probabilistic methods, ideas from the machine learning community) are likely to be increasingly applied in computational semantics. Most important, computational semantics seems to have reached the stage where the exploration and development of inference is one of its most pressing tasks and a lot of interesting new work is taking inferential issues seriously.

    ICoS-4 is intended to bring together researchers from areas such as computational linguistics, artificial intelligence, computer science, and logic, in order to discuss approaches and applications of Inference in natural language semantics.

    Two kinds of submission are invited:

    Submission deadline is June 30, 2003. Submission is by e-mail. Either Postscript or PDF files can be sent to icos4@aplog.org.

    The workshop proceedings will be distributed at the conference; plans are also under way to publish a selection of accepted papers as a special journal issue.

    For further information, see the Web site.

    New Book

    An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edition by Peter B. Andrews

    This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's unifying principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's theorem, unification, duality, interpolation, and definability.

    The last three chapters of the book provide an introduction to type theory (higher-order logic). The author shows how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models, which is important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's paradox about countable models of set theory.

    Some of the numerous exercises require giving formal proofs. A computer program called ETPS, available from the Web, facilitates doing and checking such exercises.

    This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification.

    Kluwer Academic Publishers, Dordrecht
    Hardbound, ISBN 1-4020-0763-9
    408 pages; EUR 88.00 / USD 81.00 / GBP 55.00

    Call for Contributions: QPQ Deductive Software Repository


    QPQ is an open source repository for deductive software components. It represents a community effort for publishing, preserving, and maintaining high-quality deductive software in source code form. Dr. Mark Stickel is the editor-in-chief of QPQ.

    Submissions of deductive software systems, components, and applications are welcome; the submissions must be relevant to automated deduction. Examples include matching and unification procedures, rewrite engines, BDD packages, SAT solvers, model checking tools, decision procedures, induction analyzers, proof search engines, term indexing libraries, benchmark suites, formalization libraries, editors and user interface tools, language processors, program synthesis and transformation systems, and innovative applications. Authors may choose to have their submissions refereed for design, functionality, efficiency, and documentation. Accepted submissions will be published through the QPQ Web site. For more information regarding membership in the repository and submission and editorial guidelines, visit the QPQ Web site. The QPQ Manifesto can be read at the Web site.

    A workshop on the QPQ deductive software repository will be held on July 28, 2003, as part of the CADE-19 conference at Miami, Florida.



    Open Question

    Larry Wos
    E-mail wos@mcs.anl.gov

    In combinatory logic, various fragments are studied in terms of specific combinators. A particularly difficult problem in this area has focused on the basis consisting of S and K alone, which provides a basis for all of combinatory logic. Sxyz = xz(yz) and Kxy = x. (By convention, all expressions are left associated unless otherwise indicated.) Of interest is whether the strong fixed point property holds for the fragment whose basis consists of S and K alone. To be such a fixed point combinator F, it must be that Fy = y(Fy) for all y.

    You are presented specifically with three challenges:

    1. Prove that such an F exists in terms of S and K.

    2. Using an automated reasoning program and without guidance, find such a combinator.

    3. John Tromp found a combinator of length 12. Using an automated reasoning program, find a combinator of length 12 or shorter. Even better, prove that no shorter one exists, or find a shorter one.


    Gail Pieper
    June 2003