AARNEWS - February 2005

ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 66, February 2005

From the AAR President
Herbrand Award: Call for Nominations
Fascinating XCB Inference
Call for Papers

  • ESCAR
  • ARSPA'05
  • CSL'05
  • SEFM 2005
  • TABLEAUX 2005

  • E. W. Beth Dissertation Prize

    From the AAR President, Larry Wos...

    I am most pleased to see in this first issue of 2005 an article by my colleague William McCune, in which he reports on an automatic proof of XCB--a proof dear to my heart!

    I also call your attention to two other articles of particular interest. Both are calls for nominations for awards: one for the Herbrand Award for exceptional contributions to the field of automated deduction, the other for the E. W. Beth Dissertation Award for the best dissertation in logic, language, and information in the year 2004. Such prizes pay tribute to both those experienced in the field and those new to the field.

    Herbrand Award: Call for Nominations

    Amy Felty
    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)
    Gerard Huet (1998)
    Robert S. Boyer and J Strother Moore (1999)
    William W. McCune (2000)
    Donald W. Loveland (2001)
    Mark E. Stickel (2002)
    Peter B. Andrews (2003)
    Harald Ganzinger (2004)

    A nomination is required for consideration for the Herbrand award.

    The deadline for nominations for the Herbrand Award that will be given at CADE 2005 is April 1, 2005. Nominations pending from previous years must be resubmitted in order to be considered.

    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 Franz Baader, President of CADE Inc. (baader@tcs.inf.tu-dresden.de), with copies to afelty@site.uottawa.ca.

    Fascinating XCB Inference


    William McCune
    mccune@mcs.anl.gov

    A long-standing question in propositional logic was answered in 2002 by Larry Wos [2]. The question was whether the formula XCB,

    \begin{displaymath}
e(x,e(e(e(x,y),e(z,y)),z)),
\end{displaymath} (1)

    is a single axiom for the the equivalential calculus (EC). The formula XCB was the last formula of its length to be classified: thirteen EC theorems of that length were known to be single axioms, and all other EC theorems of that length were known to be too weak to be single axioms.

    The problem can be stated easily in first-order logic. Because the pair of axioms {symmetry, transitivity} is a basis for EC, the following clauses represent the problem (x, y, z are variables, and a, b, c are constants).

        -P(e(x,y)) | -P(x) | P(y).      % condensed detachment
        P(e(x,e(e(e(x,y),e(z,y)),z))).  % XCB
        -P(e(e(a,b),e(b,a))) | -P(e(e(a,b),e(e(b,c),e(a,c)))).  % denial
    
    Hyperresolution is typically used for problems of this type, and the goal was to derive symmetry and transitivity from XCB by hyperresolution with condensed detachment.

    Wos proved the theorem with a sequence of Otter searches, first proving short EC theorems and then using the proofs to guide subsequent searches. Many search strategies were used, including resonance, the hot list, and not allowing formulas containing instances of $e(x,x)$ [1]. In addition, the search strategy was changed from one search to the next, with various combinations of the weight threshold (max_weight), the age-weight ratio (pick_given_ratio), and other parameters. The first proof Wos found has 71 steps; he then simplified it to 25 steps (see the proof in [2]). Later he found a 23-step proof.

    All of Wos's proofs were derived from his original 71-step proof. The 71-step proof and the 25-step proof contain a fascinating inference:

    A.  P(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,v6),e(v7,
             v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)).
    B.  P(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e(v6,w)),
             v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))).
    C.  [from A and B] P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))).
    
    Clause A is the major premise (it unifies with the first literal of condensed detachment), and clause B is the minor premise (it unifies with the second literal). If one constructs the instance of the major premise from the most general unifier, it contains 2,940 symbols! Wos's 23-step proof has a similar inference, with the same conclusion but with different major and minor premises:
    A2. P(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(v,e(e(e(v,w),e(v6,w)),v6)),
       x))),e(v7,e(e(e(v7,v8),e(v9,v8)),v9))),v10),e(v11,v10)),v11)).
    B2. P(e(e(x,e(e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),y),w),e(v6,w)),v6)),x)),
       e(v7,e(e(e(v7,v8),e(v9,v8)),v9)))).  
    C.  [from A2 and B2] P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))).
    

    The instance of the major premise for this inference has 1,928 symbols.

    Although a human might never find a proof with such complex inferences, they are trivial for a program. What makes these particular proofs difficult for our programs to find are premises A, A2, B, and B2 themselves. Clauses are typically selected for inference if they are short or if they appear early in the search (as determined by the pick_given_ratio). These premises have neither property.

    I wished to find an automatic proof (without using guidance from any of Wos's proofs) and, if successful, to see whether the proof had such complex inferences. Because Wos's original proof was found in such an roundabout way, I hoped that any proofs found independently would be substantially different.

    I ran a set of searches with various combinations of the basic search parameters and with the strategy of deleting clauses containing instances of $e(x,x)$. The searches were automatic (trying to prove the whole theorem) and independent, as opposed to Wos's iterative approach. One search succeeded, producing a proof in about ten minutes.

    Does the new proof contain such a complex inference? Yes, and it is exactly the same inference (same premises, same conclusion) as in Wos's 23-step proof. The conclusion seems to be a key step.

    In addition, I found by exhaustive search that if the weight threshold is less than 48 (the weight of clauses A, A2, and B above), and if clauses containing instances of $e(x,x)$ are deleted, then no proofs can be found.

    Otter input files, output files, proofs, and the instances corresponding to the complex inferences can be found on the Web.

    Bibliography

    1 W. McCune and L. Wos. Experiments in automated deduction with condensed detachment. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 607, pages 209-223, Berlin, 1992. Springer-Verlag.

    2 L. Wos, D. Ulrich, and B. Fitelson. Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus. J. Automated Reasoning, 29(2):107-124, 2002.

    Call for Papers

    ESCAR

    The CADE-20 Workshop on Empirically Successful Classical Automated Reasoning (ESCAR) will bring together practioners and researchers who are concerned with the implementation and deployment of working automated reasoning systems for classical logic (propositional, first order, and higher order). The workshop will discuss "really running" systems, and not theoretical ideas that have not yet been translated into working software. ESCAR is the successor to the successful ESFOR workshop held at IJCAR 2004, CADE-20 will be held July 22-27, 2005; ESCAR will be held on July 22-23. Full details are available at the Web.

    Submission of papers for presentation at the workshop, and proposals for system and application demonstrations at the workshop, are now invited. Submissions will be refereed, and a balanced program of high-quality contributions will be selected. The submission deadline is May 1.

    Additionally, the Journal of Automated Reasoning has agreed to a special issue on empirically successful automated reasoning. Authors of ESCAR papers will be able to submit extended versions of their workshop papers for this special issue. All papers submitted for the special issue will be reviewed according to the journal's standards.

    ARSPA'05

    The second workshop on Automated Reasoning for Security Protocol Analysis (ARSPA'05) will be held in Lisboa, Portugal, July 16, 2005 (co-located with ICALP'05). The ARSPA workshop aims to bring together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. The submission deadline is April 15, 2005. For more details see the Web page.

    CSL'05

    Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic. CSL'05 will take place August 22-25, 2005, at Oxford, UK. The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Suggested topics of interest include automated deduction and interactive theorem proving, constructive mathematics and type theory, equational logic and term rewriting, modal and temporal logic, model checking, logical aspects of computational complexity, finite model theory, computational proof theory, logic programming and constraints, lambda calculus and combinatory logic, categorical logic and topological semantics, domain theory, database theory, specification, extraction and transformation of programs, logical foundations of programming paradigms, linear logic, and higher-order logic.

    The deadline for abstracts is March 25, 2005; the deadline for papers April 1, 2005 The proceedings will be published in the Springer Lecture Notes in Computer Science. For more information, please see the Web page.

    Special Award

    The EACSL Board has decided to launch the Ackermann Award: The EACSL Outstanding Dissertation Award for Logic in Computer Science. The first awards will be presented to the recipients at CSL'05. Further details of the Award can be found at the Web page.

    SEFM 2005

    The Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005) will be held in Koblenz, Germany, September 7-9, 2005. The aim of the conference is to bring together practitioners and researchers from academia, industry, and government to advance the state of the art in formal methods, to scale up their application in software industry, and to encourage their integration with practical engineering methods.

    Topics of particular interest to AAR memberrs are software specification, validation and verification and integration of formal and informal methods or different formal methods, and model checking and theorem proving. Substantial experience reports and case studies are particularly welcome.

    The proceedings of the conference will be published by the IEEE Computer Society Press. The best papers will be selected to be published in revised and extended version in the International Journal on Software and Systems Modelling.

    The submission deadline is March 18, 2005, for titles and abstracts, and April 1, 2005, for papers. For further information see the Web site.

    TABLEAUX 2005

    TABLEAUX 2005 is a continuation of international meetings on automated reasoning with analytic tableaux and related methods. On September 14-17, 2005, the conference will be held in Koblenz, Germany. The International Workshop on First-Order Theorem Proving (FTP 2005) will also be held in Koblenz at the same time, with opportunities for joint registration.

    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. Topics of interest for TABLEAUX 2005 include the following:

    TABLEAUX 2005 puts a special emphasis on applications. Papers describing applications of tableaux and related methods in areas such as hardware and software verification, knowledge engineering, and the semantic Web are particularly invited. Accepted papers in these categories will be published in the conference proceedings (within the LNAI series of Springer).

    The submission deadline is March 31, 2005, for tutorial proposals and April 30, 2005, for papers. For further information see the conference Web site.

    E. W. Beth Dissertation Prize
    Call for Submissions

    Since 2002, FoLLI (the Association of Logic, Language, and Information, www.folli.org) awards the E. W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. Submissions are invited for 2005. The prize will be awarded to the best dissertation which resulted in a Ph.D. in the year 2004. The dissertations will be judged on the impact they made in their respective fields, breadth and originality of the work, and also on the interdisciplinarity of the work. Ideally the winning dissertation will be of interest to researchers in all three fields.

    Who qualifies: Those who were awarded a Ph.D. degree in the areas of logic, language, or information between January 1, 2004, and December 31, 2004. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. However, after a careful consideration, FoLLI has decided to accept only dissertations written in English.

    Prize: The prize consists of a certificate, an invitation to present the thesis during ESSLLI 05, a donation of 2500 euros provided by the E. W. Beth Foundation, fee waive for ESSLLI 05 attendance, and the possibility to publish the thesis (or a revised version of it) in the new series of books in Logic, Language and Information to be published by Springer-Verlag as part of LNCS or LNCS/LNAI. (Further information on this series will be posted on the FoLLI site soon.)

    How to submit: We accept only electronic submissions. The following documents are required:

    1. the thesis in pdf or ps format (doc/rtf not accepted);

    2. a ten-page abstract of the dissertation in ascii or pdf format;
    3. a letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded;
    4. two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree.

    All documents must be submitted electronically to beth_award@dimi.uniud.it. If you experience any problems with the email submission or do not receive a notification from us within three working days, please write to policriti@dimi.uniud.it or folli@inf.unibz.it.

    The deadline for submissions is March 15, 2005.

    The prize will be officially assigned to the winner at ESSLLI'05, the 17th European Summer School in Logic, Language, and Information, to be held in Edinburgh, Scotland, August 9-19, 2005. The prize winner will be expected to attend the ceremony and to give a presentation of the Ph.D. dissertation at ESSLLI'05.


    Gail W. Pieper
    pieper@mcs.anl.gov
    February 2005