# ASSOCIATION FOR AUTOMATED REASONING

## From the AAR President, Larry Wos...

My great thanks for the splendid contribution of Wolfgang Ahrendt in his role as secretary to AAR. He has provided much inspiration, and he will indeed be missed.

Consistent with recent columns, I offer the following challenge, taken from abstract algebra:

A group is a nonempty set with a binary operation, called multiplication or addition. With respect to that operation, the set (typically) admits a two-sided identity, a two-sided inverse (with respect to the identity), and associativity. Other definitions exist. Many years ago, William McCune (author of OTTER) studied the possibility of finding single axioms in various areas. He was monumentally successful. In particular, he found single axioms for groups of exponent 3. A group has exponent 3 if and only if the third power of x, for every element x, is the identity e.

You are asked to prove that the following equation is a single axiom for groups of exponent 15.

```(f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(x
,f
(f
(x
,y
),z
)))))))),f
(e
,f
(z
,f
(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,z))))))))))))))))))))))
= y).
```

The following correspond to the (negations of the) targets.

```(f(f(a,b),c) != f(a,f(b,c))) | \$Ans(assoc).
(f
(a
,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))))))))) !
= e) | \$Ans(exp15).
(f(e,a) != a) | \$ANS(lid).
(f(a,e) != a) | \$ANS(rid).
```

Of course, you might choose to rely on paramodulation with various strategies, or perhaps on a Knuth-Bendix approach.

While I labeled this a challenge, perhaps I should qualify what I meant. The theorem has been proved: that is, all four properties have been deduced. What I am asking you to do is use your own program to find the proof.

For a related challenge, but one that might indeed prove more difficult, you are asked to find a different single axiom for groups of exponent 15. (I know there is at least one other).

## Herbrand Award: Call for Nominations

Martin Giese
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honour 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)
• Martin Davis (2005)
• Wolfgang Bibel (2006)
• Alan Bundy (2007)
• Edmund Clarke (2008)
• Deepak Kapur (2009)
• David Plaisted (2010)

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE 23 is:

1st April, 2011

Nominations pending from previous years must be resubmitted in order to be considered.

Nominations should consist of a letter (preferably email) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

with copies to

martingi (at) ifi.uio.no

Maria Paola Bonacina's term as CADE trustee expired after the trustee elections in 2010, and this also ended her term of service as president. The Board of Trustees has elected Franz Baader as new president of CADE.

On behalf of CADE and AAR, I congratulate Franz Baader on his reelection as president, and wish him another successful term of service.

Also on behalf of the AAR and CADE, I would like to thank Maria Paola Bonacina for her service and commitment as president of CADE during the past years.

Martin Giese

## New AAR and CADE Secretary

Larry Wos
(AAR President)

After four years of excellent service, Wolfgang Ahrendt has resigned from the posts of AAR and CADE secretary. The AAR Board and the CADE Board of Trustees cannot express how valuable has been his service to the community. He will be missed in this capacity. Thank you, Wolfgang, for everything; it was a pleasure to work with you.

Our new AAR secretary/treasurer and CADE secretary is Martin Giese. We welcome Martin in his new role and look forward to working with him.

## New CADE representatives on AAR board

Apart from the president, vice president, and secretary, there are always two CADE nominees on the AAR board. These nominees are delegates chosen by the CADE board of trustees. Until recently, Maria Paola Bonacina and Geoff Sutcliffe have filled these positions, but both are now no longer members of the CADE board of trustees.

The CADE board of trustees has elected Reiner Hähnle and Neil Murray to be the new CADE representatives on the AAR board.

I would like to thank the previous delegates for their service on the board of the AAR!

Martin Giese

Although Geoff Sutcliffe is no longer on the CADE board of trustees, nor on the AAR board, he has agreed to continue administrating the CADE and AAR web pages and mailing lists.

On behalf of CADE and AAR, I would like to thank him for continuing this valuable service to our community!

Martin Giese

## Conferences

The 23rd Conference on Automated Deduction will include an attractive array of satellite workshops, including workshops, tutorials, and of course a competition.

Detailed information about these events will be published in the next AAR Newsletter. In the meantime, refer to the CADE 23 satellite event web page for up to date information.

#### Workshops

• The 25th International Workshop on Unification (UNIF), organized by Franz Baader, Barbara Morawska, Jan Otop, see also below.
• The First Workshop on Automated Theory Engineering (ATE), organized by Peter Höfner, Annabelle McIver, Georg Struth.
• Workshop on Proof eXchange for Theorem Proving (PxTP), organized by Pascal Fontaine, Aaron Stump.
• Proof Search in Axiomatic Theories and Type Theories (PSATTT), organized by Stéphane Lengrand, Assia Mahboubi, Germain Faure.
• The Boogie Workshop, organized by Rustan Leino, Michal Moskal, Shaz Qadeer.
• Workshop on CTP Components for Education Software (CTP-edu), organized by Walther Neuper.

#### Competitions

• The 23rd CADE ATP System Competition (CASC-23), organized by Geoff Sutcliffe.

#### Tutorials

• The Relevance of Automated Reasoning to Human Thinking, presented by Robert Kowalski.
• Practical Computer Formalization of Mathematics using Mizar, presented by Jesse Alama, Adam Grabowski, Artur Kornilowicz, Adam Naumowicz, Piotr Rudnicki, Josef Urban.
• First-order theorem proving and Vampire, presented by Krystof Hoder, Laura Kovacs, Andrei Voronkov.
• Practical reasoning with Quantified Boolean Formulas, presented by Luca Pulina, Martina Seidl, Armando Tacchella.
• Grammatical Framework: A Hands-On Introduction, presented by Aarne Ranta.
• Model Checking Modulo Theories: Theory and Practice, presented by Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina.

### ITP 2011, Interactive Theorem Proving

ITP 2011 will take place in Nijmegen, The Netherlands, on 22–25 August 2011, follows by workshops on 26–27 August.

ITP is an international conference on Interactive Theorem Proving and related issues including applications, case studies, foundations, languages, and implementations. It is a combination of the TPHOLs (Theorem Proving in Higher Order Logics) conferences and the ACL2 Workshop series. ITP 2011 is the second ITP conference; ITP 2010 was held in Edinburgh as part of FLoC 2010.

Important dates:

• Abstract submission deadline: 13 February 2011
• Paper submission deadline: 20 February 2011

Full details are available on the ITP website.

### TAP'11, Tests & Proofs

The 5th International Conference on Tests & Proofs will be held in Zurich, Switzerland, on June 30–July 01, 2011, as part of the TOOLS Federated Conferences 2011.

The TAP conference is devoted to the convergence of proofs and tests, usually considered diagonally opposed approaches to ensuring software quality. Any work that combines theorem proving techniques for software correctness with testing techniques is of interest.

Research papers of up to 16 pages, and short papers of up to 6 pages should be submitted until 11 February, abstracts are due on 4 February 2011.

Full information is available on the conference web site.

### CSL'11, Computer Science Logic

The 20th EACSL Annual Conference on Computer Science Logic (CSL'11) will be held in Bergen, Norway, on 12–15 September 2011. CSL is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. The Ackermann Award for 2011 will be presented to the recipients at CSL 2011.

Topics of interest include automated deduction and interactive theorem proving for a variety of logics, and many more which will be relevant for many in the AR community.

Papers should be submitted until 27 March 2011. The proceedings will be published in the series LIPIcs, Leibniz International Proceedings in Informatics.

See the conference web page for full details.

### SEFM 2011, Software Engineering and Formal Methods

The 9th International Conference on Software Engineering and Formal Methods will take place in Montevideo, Uruguay, on 14–18 November 2011.

The aim of the conference is to bring together researchers and practitioners 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. Authors are invited to submit both research and tool papers.

The topics of interest include all kinds of formal methods related to the construction of software, including in particular methods based on theorem proving.

Important dates:

• Abstract submission deadline: 23 April 2011
• Paper submission deadline: 30 April 2011

Full details are available on the conference web site.

## Workshops

### UNIF 2011, Intl. Workshop on Unification

UNIF 2011 is the 25th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of identifying given terms, either syntactically or modulo an equational theory. The aim of UNIF 2011, as that of the previous meetings, is to to bring together researchers interested in unification theory and related topics, to present recent (even unfinished) work, and discuss new ideas and trends in this and related fields.

Submissions not exceeding 5 pages should be submitted until 2 May. Please refer to the workshop web page for more information.

## Special Issue on Specification and Verification of Web Systems

The Journal of Symbolic Computation will publish a special issue on automated specification and verification of web systems, edited by Laura Kovács and Temur Kutsia.

The special issue is related to the topics of the workshop WWV'10: Automated Specification and Verification of Web Systems, which took place in Vienna on 30–31 July 2010. Both participants of the workshop and other authors are invited to submit contributions.

The increased complexity of Web sites and the explosive growth of Web-based applications has turned their design and construction into a challenging problem. Nowadays, many companies have diverted their Web sites into interactive, completely-automated, Web-based applications (such as Amazon, on-line banking, or travel agencies) with a high complexity that requires appropriate specification and verification techniques and tools. Systematic, formal approaches to the analysis and verification can address the problems of this particular domain with automated and reliable tools that also incorporate semantic aspects.

Papers relevant to this topic shall be submitted until 7 March 2011.

See here for full details.

## PhD positions in Symbolic Computation

The Research Institute for Symbolic Computation (RISC) at the Johannes Kepler University in Linz, Austria, is an international institute with its research focus on various branches of symbolic computation. This includes, amongst others, automated reasoning and formal methods. RISC has had a special PhD programme in Symbolic Computation for almost twenty years.

Students who are interested in starting their PhD studies at RISC in October 2011 should send their application before February 15, 2011.

## PhD and Postdoc positions in Rigorous Systems Engineering

The RiSE project is a National Research Network funded by the Austrian National Science Foundation (FWF) on the topic of Rigorous Systems Engineering.

RiSE is concerned with improving the quality of complex software systems. It aims to move beyond classical, a posteriori verification techniques such as model checking, to an integrated approach of system design and formal verification.

RiSE is looking for several postdocs and PhD students in formal methods, systems engineering and related fields such as programming languages and distributed systems, to work on topics such as:

• design and verification of concurrent and real-time software;
• reactive synthesis and game theory;
• logical decision procedures.

The earliest starting date for PhD and Post-doc positions is 1 March 2011.

Martin Giese

An election was held from November 30 through December 19 to fill three positions on the board of trustees of CADE Inc. Franz Baader, Clark Barrett, Amy Felty, Jürgen Giesl, Konstantin Korovin, Larry Paulson, and Brigitte Pientka were nominated for these positions. (See AAR Newsletter No. 89, October 2010.)

Ballots were sent by electronic mail to all members of AAR on November 30, for a total of 812 ballots. Of these, 108 were returned with a vote, representing a participation level of 13.3% (as compared to 18.3% in 2009, 18% in 2008, 16.4% in 2007, 16.0% in 2006, and 18.1% in 2005). All votes were valid. Therefore, in each iteration of the STV algorithm (as described in the CADE Bylaws, see here), a candidate is elected iff she or he gets strictly more than 54 1st preference votes. Otherwise, the votes of the candidate with the least 1st preference votes are redistributed.

The following table reports the initial distribution of preferences among the candidates:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 27 22 17 16 4 3 19 108 C. Barrett 5 8 8 7 13 5 62 108 A. Felty 11 20 22 8 5 7 35 108 J. Giesl 9 20 14 16 13 7 29 108 K. Korovin 9 7 13 13 5 9 52 108 L. Paulson 35 16 10 3 9 4 31 108 B. Pientka 12 15 19 14 7 6 35 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of C. Barrett, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 29 25 16 13 4 9 12 108 A. Felty 11 20 23 9 8 18 19 108 J. Giesl 10 21 17 16 12 9 23 108 K. Korovin 10 8 15 11 10 23 31 108 L. Paulson 36 16 9 5 11 15 16 108 B. Pientka 12 16 20 17 7 15 21 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of K. Korovin, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 32 26 14 15 5 11 5 108 A. Felty 13 21 23 12 14 18 7 108 J. Giesl 10 28 17 13 13 14 13 108 L. Paulson 38 15 10 6 16 14 9 108 B. Pientka 15 14 26 16 9 22 6 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of J. Giesl, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 40 24 15 13 7 5 4 108 A. Felty 13 30 22 18 9 16 0 108 L. Paulson 39 18 11 17 11 11 1 108 B. Pientka 16 23 26 14 13 14 2 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of A. Felty, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 41 33 18 6 4 6 0 108 L. Paulson 41 24 17 9 9 8 0 108 B. Pientka 24 31 23 7 11 12 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of B. Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 52 40 3 5 6 2 0 108 L. Paulson 51 31 5 7 12 2 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of L. Paulson, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total F. Baader 92 1 5 7 3 0 0 108

Now, F. Baader reaches more than 54 first preference votes, and is elected to the board of trustees. To find the second elected candidate, we redistribute his votes and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total C. Barrett 6 10 10 14 6 50 12 108 A. Felty 16 28 16 6 6 33 3 108 J. Giesl 20 16 17 16 10 21 8 108 K. Korovin 10 14 15 8 7 45 9 108 L. Paulson 43 13 7 8 6 26 5 108 B. Pientka 13 25 19 9 7 28 7 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of C. Barrett, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 16 29 17 8 18 18 2 108 J. Giesl 22 16 23 13 10 17 7 108 K. Korovin 12 17 12 11 21 30 5 108 L. Paulson 44 13 6 14 13 15 3 108 B. Pientka 13 27 23 8 14 18 5 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of K. Korovin, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 20 28 20 15 15 10 0 108 J. Giesl 24 24 17 16 10 13 4 108 L. Paulson 47 10 11 17 10 12 1 108 B. Pientka 16 30 24 10 15 13 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of B. Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 24 39 19 4 17 5 0 108 J. Giesl 33 26 21 4 15 9 0 108 L. Paulson 50 17 17 3 17 4 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of A. Felty, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total J. Giesl 45 35 3 10 13 2 0 108 L. Paulson 59 23 4 7 14 1 0 108

Now, L. Paulson reaches more than 54 first preference votes, and is elected to the board of trustees. To find the third elected candidate, we redistribute his votes and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total C. Barrett 12 8 15 9 39 22 3 108 A. Felty 34 20 10 7 19 18 0 108 J. Giesl 26 17 22 13 19 10 1 108 K. Korovin 18 17 9 10 32 19 3 108 B. Pientka 18 34 12 8 19 15 2 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of C. Barrett, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 34 22 12 13 17 10 0 108 J. Giesl 30 17 26 10 16 8 1 108 K. Korovin 23 14 14 17 25 14 1 108 B. Pientka 19 39 11 10 20 7 2 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of B. Pientka, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 45 19 17 4 18 5 0 108 J. Giesl 36 33 13 7 17 1 1 108 K. Korovin 24 23 21 13 25 2 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of K. Korovin, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 52 28 5 7 15 1 0 108 J. Giesl 47 33 3 14 10 1 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of J. Giesl, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total A. Felty 80 4 3 17 4 0 0 108

Now, A. Felty reaches more than 54 first preference votes, and is elected to the board of trustees. To find the fourth elected candidate, we redistribute her votes and get the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total C. Barrett 16 14 11 33 21 13 0 108 J. Giesl 31 26 20 14 13 4 0 108 K. Korovin 22 18 11 33 10 14 0 108 B. Pientka 37 23 8 16 11 13 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of C. Barrett, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total J. Giesl 36 31 15 10 14 2 0 108 K. Korovin 27 19 21 20 14 7 0 108 B. Pientka 41 23 15 7 15 7 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of K. Korovin, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total J. Giesl 45 36 2 16 9 0 0 108 B. Pientka 50 29 1 15 12 1 0 108

No candidate reaches more than 54 first preference votes. By redistributing the votes of J. Giesl, one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total B. Pientka 78 1 9 15 5 0 0 108

Now, B. Pientka reaches more than 54 first preference votes, and is elected to the board of trustees.

To summarise, the four candidates elected to the board of trustees are Franz Baader, Larry Paulson, Amy Felty, and Brigitte Pientka.

After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:

• Christoph Benzmüller (elected 2008)
• Nikolaj Bjørner (CADE-23 program co-chair)
• Amy Felty (elected 2007, reelected 2010)
• Martin Giese (Secretary)
• Rajeev Goré (elected 2009)
• Reiner Hähnle (Vice President, elected 2005, reelected 2008)
• Neil Murray (Treasurer)
• Larry Paulson (elected 2010)
• Brigitte Pientka (elected 2010)
• Renate Schmidt (elected 2009)
• Viorica Sofronie-Stokkermans (CADE-23 program co-chair)
• Christoph Weidenbach (elected 2009)

On behalf of the AAR and CADE Inc., I thank Maria Paola Bonacina, Geoff Sutcliffe, Andrei Voronkov, and Jürgen Giesl for their service as trustees during the past years, and all candidates for running in the election, all the members who voted; and offer congratulations to Franz Baader, Larry Paulson, Amy Felty, and Brigitte Pientka on being elected.