NEWSLETTER

From the AAR President

Herbrand Award:
Call for Nominations

Fascinating XCB Inference

Call for Papers

E. W. Beth Dissertation Prize

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.

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)

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.

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

(1) |

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)))). % denialHyperresolution 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 [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 . 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 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.

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.

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.

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.

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

- analytic tableaux for various logics (theory and applications)
- related techniques and concepts, for example, model checking and BDDs
- related methods (model elimination, sequent calculi, connection method, etc.)
- new calculi and methods for theorem proving in classical and nonclassical logics (modal, description, intuitionistic, linear, temporal, etc.)
- systems, tools, implementations, and applications

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.

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:

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

- a ten-page abstract of the dissertation in ascii or pdf format;
- 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;
- 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.

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