ASSOCIATION FOR AUTOMATED REASONING

• From the AAR President, Larry Wos...
• Herbrand Award: Call for Nominations
• Franz Baader succeeds Maria Paola Bonacina as President of CADE
• New AAR and CADE Secretary
• New CADE representatives on AAR board
• CADE and AAR Webmaster
• Conferences
  • CADE 23 Satellite Events
  • ITP 2011, Interactive Theorem Proving
  • TAP'11, Tests & Proofs
  • CSL'11, Computer Science Logic
  • SEFM 2011, Software Engineering and Formal Methods
• Workshops
  • UNIF 2011, Intl. Workshop on Unification
• Special Issue on Specification and Verification of Web Systems
• PhD positions in Symbolic Computation
• PhD and Postdoc positions in Rigorous Systems Engineering
• Results of CADE Elections

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

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

Franz Baader, President of CADE Inc.
baader (at) tcs.inf.tu-dresden.de

with copies to

martingi (at) ifi.uio.no

Franz Baader succeeds Maria Paola Bonacina as President of CADE

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
(Secretary of AAR and CADE)

New AAR and CADE Secretary

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
(Secretary of AAR and CADE)

CADE and AAR Webmaster

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
(Secretary of AAR and CADE)

Conferences

CADE 23 Satellite Events

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.

More information about doctoral studies at RISC can be found here.

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.

More information, in particular about requirements and application procedure can be found here.

Results of CADE Elections

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:

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

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

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

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

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

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

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:

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

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

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

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

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:

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

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

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

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

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:

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

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

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

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

• Franz Baader (elected 2010)
• 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.