NEWSLETTER No. 94, December 2011

- From the AAR President, Larry Wos...
- A Note on Identities in Groups and Semigroups
- Conferences
- Workshops
- Winter School on Verification
- IFCoLog ACDC, a financial service for communities
- Call for Papers: “Automated Reasoning and Mathematics: Essays in Memory of William McCune”
- RISC ProgramExplorer 1.0
- Results of CADE Elections

A long, long, long time ago, Raymond Smullyan and I were graduate students in the Mathematics Department at the University of Chicago. Our paths did not cross again until the 1980s, when I learned of a charming book he had written on combinatory logic, “To Mock a Mockingbird.” Roger Hindley, in answer to a question I posed, in effect said that combinators are not defined (as groups and rings are) but instead are presented as equations. Such equations are left-associated, unless otherwise indicated.

For example, the combinator *B* is presented with the equation
*Bxyz = x(yz)*, for all combinatory expressions,
*x*, *y*, and *z*.
Another interesting combinator is *M*, with *Mx = xx*.
When last I checked, an open question exists for the fragment whose
basis consists of just *B* and *M*.
For the open question, the following is relevant.
Where *A*
is a given fragment with basis *B*, the strong fixed point
property holds for *A*
if and only if there exists a combinator *y*
such
that, for all combinators
*x*, *yx = x(yx)*, where *y*
is expressed purely
in terms of elements of *B*.
The open question: Does the *B*-and-*M*
fragment satisfy the strong fixed
point property?
Be warned that this question has resisted efforts by fine minds.

Here you are asked to find one or more fixed point combinators,
expressed solely in terms of the combinators
*B* and *N*, with *Nxyz = xzyz*.
To get started, you might seek a fixed point combinator for the
*B*-and-*W*
fragment, where *Wxy = xyy*.
Such combinators do exist, but none were known before the mid-1980s.
To illustrate that all is indeed complex, I note that the
*B*-and-*L*
fragment does not satisfy the fixed point property, where
*Lxy = x(yy)*.
Yes, the grouping (of symbols) for subexpressions changes things dramatically
in some cases.
You might enjoy trying to prove that the
*B*-and-*L*
fragment fails to satisfy the strong fixed pount property.

Identities of the form `yx = xU(x,y)y`

have the unusual
property that if they imply `yx = xy`

in groups, then they
also imply it in semigroups. It is much easier to work in groups
because they have an identity element, inverses, and the cancellation
property. However, in semigroups one has only one tool, substitutions
using the given identity. This contrast enables one to construct identities that
imply `yx = xy`

yet not know which sequence of
substitutions transforms `yx`

to `xy`

.

In a paper published on ArXiv
I discuss a variety of
examples. AI specialists may find shorter proofs than the ones I found
and explore other examples. They may also find of interest my earlier
paper, The Combinatorial Degree of Proofs and Equations, *Algebra
Universalis* 35 (1996) 472–484.

IJCAR 2012 will take place in Manchester, UK, on June 26–July 1, 2012. IJCAR will be held as part of the Alan Turing Year 2012, just after The Alan Turing Centenary Conference in Manchester.

IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks. IJCAR 2012 is a merger of leading events in automated reasoning:

- CADE (Conference on Automated Deduction),
- FroCoS (Workshop on Frontiers of Combining Systems),
- FTP (Workshop on First-order Theorem Proving), and
- TABLEAUX (Conference on Analytic Tableaux and Related Methods)

IJCAR 2012 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited. The proceedings of IJCAR 2012 will be published by Springer-Verlag in the LNAI/LNCS series.

Important dates:

- Abstract submission deadline: January 23, 2012
- Paper submission deadline: January 30, 2012
- Notification of paper decisions: March 26, 2012
- Final version of papers due: April 16, 2012

Full details are available on the IJCAR website.

The fourth NASA Formal Methods Symposium will take place in Norfolk, Virginia, USA on April 3–5, 2012. The Symposium is a forum with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Theorem proving is listed amongst the topics of interests.

Regular papers of up to 15 pages and tool papers of up to 6 pages are to be submitted until December 11, 2011. The proceedings will be published in Springer's LNCS series.

See the symposium web site for details.

RTA 2012 will take place in Nagoya, Japan, on May 28–June 2, 2012.

RTA is the major conference on rewriting and covers all aspects related to rewriting such as termination, equational reasoning, theorem proving, Lambda calculus, higher-order rewriting, unification, verification, constraints, and software tools.

Important Dates:

- Abstract submission: January 4, 2012
- Paper submission January 9, 2012
- Notification: March 2, 2012
- Final version: March 26, 2012

Full details are available on the RTA website.

The 3rd International Conference on Interactive Theorem Proving will be held in Princeton, New Jersey, USA on 13–16 August 2012.

The program committee welcomes submissions on all aspects of interactive theorem proving and its applications. Submission categories include regular papers and "rough diamonds". Important dates:

- Abstract submission deadline: 6 February 2012
- Paper submission deadline: 13 February 2012

Full details are available on the conference web site.

The 19th Workshop on Logic, Language, Information and Computation will be held at the University of Buenos Aires, Argentina, from September 3–6, 2012. WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning.

A title and single-paragraph abstract should be submitted by April 27, and the full paper of up to 10 pages (excluding references) by May 4. The proceedings will be published in Springer's LNCS series.

Refer to the conference web site for full details, including submission instructions.

IWIL-2012, the 9th International Workshop on the Implementation of Logics will be held in Merida, Venezuela, on March 10, 2012, in conjunction with the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR).

IWIL asks for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies.

Position statements (2 pages), short papers (up to 5 pages), amd full papers (up to 15 pages) in Easychair format should be submitted until January 17, 2012.

See the workshop web page for full details.

APS-6, the 6th International Workshop on Analytic Proof Systems will be held in Merida, Venezuela, on March 10, 2012, in conjunction with the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR).

Analyticity is a topic that connects foundational issues in logic with applications, mainly in automated deduction and analysis of proofs. The workshop is primarily intended to enhance awareness for its topic and to promote corresponding discussions and contacts between experienced experts and younger colleagues.

Please submit a 1–2 page abstract to `analytic@logic.at`

by January 31, 2012.

See the workshop web page for full details.

The Austrian Society for Rigorous Systems Engineering (ARiSE, www.arise.or.at) and the Vienna Center for Logic and Algorithms (VCLA, www.vcla.at) are organizing a joint winter school on verification at Vienna University of Technology from 6–10 February 2012. Apart from ARiSE/VCLA students, the school will be open to outside students. A limited number of travel grants for motivated Master's and outstanding Bachelor's students is available.

The preliminary list of speakers:

- Patrice Godefroid, Microsoft Research – Invited Speaker
- Thomas A. Henzinger – Model Checking Theory
- Armin Biere – Satisfiability Solving for Propositional Logic
- Laura Kovacs – Automated Theorem Proving
- Krishnendu Chatterjee – Stochastic Games
- Christoph Kirsch – Embedded Systems
- Uwe Egly – Solving Quantified Boolean Formulas
- Ulrich Schmid – Distributed Algorithms
- Helmut Veith – Software Model Checking
- Roderick Bloem – Synthesizing Correct Systems from Specifications

Students can register for the winter school by 15 December by email to
`arise.vcla@gmail.com`

. In order to qualify for a grant, students should
submit

- A letter of motivation,
- a transcript of courses and grades with a translation into English by the applicant, and
- the name and email address of a reference person.

The student would preferably have prior knowledge of mathematical logics and/or discrete math. Decisions on grants will be made before December 23, 2011.

IFColog ACDC is a new initiative designed to help groups in computational logic administer their finances.

The declared intent of IFCoLog ACDC is to help a community, conference or group that has finances but has no treasurer or anywhere neutral and permanent to put them. For further details see the ACDC manifesto

Maria Paola Bonacina and Mark E. Stickel are in the process of editing a book of collected articles presenting research in all aspects of automated reasoning and its applications to mathematics to honor the memory of William W. (Bill) McCune and contribute to preserving his legacy.

The editors invite high-quality submissions on the general topic of automated reasoning and its applications, especially but not exclusively in mathematics, with connections to any of Bill McCune's research areas:

- Automated theorem proving
- Automated model building and constraint solving
- Implementation of and practice with automated reasoners
- Algorithmics for automated reasoners: unification, matching, rewriting, indexing
- Inference control, search plans and semantic guidance for automated reasoners
- Proof checking, proof presentation, proof explanation
- Application of automated reasoners in mathematics, logic, combinatory logic, many-valued logic, algebraic structures and their axiomatizations, set theory
- Applications related to formal methods

It is expected that the book will be published in the Festschrift subseries of the Springer LNAI/LNCS series. While it is expected that most of the papers will be regular technical papers, a few papers that combine scientific content with recollections of Bill McCune's work and personality, as can be written by those who worked with him, are also sought.

The submission deadline is March 1, 2011.

For full details, including the submission procedure, please refer to the web site for the book project

This is to announce the first release of the RISC ProgramExplorer, a computer-supported program reasoning environment for a simple programming language “MiniJava”; it incorporates the RISC ProofNavigator as a semi-automatic proving assistant. The software has been developed mainly for educational purposes; it runs on computers with x86-compatible processors under the GNU/Linux operating system and is freely available under the terms of the GNU GPL. See the screencast respectively the manual available on the web page for further information.

An election was held from September 17 through October 10, 2011 to fill two positions on the
board of trustees of Cade, Inc.
Christoph Benzmüller, Konstantin Korovin, Hans de Nivelle, Viorica Sofronie-Stokkermans, and Geoff Sutcliffe
were nominated for these positions. (See *AAR Newsletter* Nr.~93, September 2011.)
Ballots were sent by electronic mail to all members of AAR on
September 17, for a total of 858 ballots. Of these, 139 were returned with a
vote, representing a participation level of 16.2% (as compared to
13.3% in 2010,
18.3% in 2009,
18% in 2008, 16.4% in 2007,
and 16.0% in 2006). All votes were valid.
Therefore, in each iteration of the STV algorithm described in
the CADE Bylaws, a candidate is elected iff she or he gets
*at least 70* 1st preference votes. Otherwise, the votes of the
candidate(s) 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. |
no supp. |

Christoph Benzmüller | 33 | 19 | 26 | 22 | 21 | 18 |

Konstantin Korovin | 13 | 19 | 23 | 23 | 28 | 33 |

Hans de Nivelle | 22 | 27 | 24 | 26 | 19 | 21 |

Viorica Sofronie-Stokkermans | 34 | 31 | 20 | 23 | 15 | 16 |

Geoff Sutcliffe | 37 | 39 | 30 | 12 | 8 | 13 |

No candidate reaches at least 70 first preference votes.

By redistributing the votes of Konstantin Korovin, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
no supp. |

Christoph Benzmüller | 34 | 26 | 27 | 34 | 18 |

Hans de Nivelle | 24 | 30 | 37 | 27 | 21 |

Viorica Sofronie-Stokkermans | 37 | 36 | 22 | 28 | 16 |

Geoff Sutcliffe | 44 | 41 | 29 | 12 | 13 |

No candidate reaches at least 70 first preference votes.

By redistributing the votes of Hans de Nivelle, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Christoph Benzmüller | 36 | 38 | 47 | 18 |

Viorica Sofronie-Stokkermans | 49 | 35 | 39 | 16 |

Geoff Sutcliffe | 53 | 53 | 20 | 13 |

No candidate reaches at least 70 first preference votes.

By redistributing the votes of Christoph Benzmüller, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Viorica Sofronie-Stokkermans | 60 | 63 | 16 |

Geoff Sutcliffe | 76 | 50 | 13 |

Now, Geoff Sutcliffe reaches at least 70 first preference votes, and is elected.

To find the next elected candidate, we redistribute the votes of Geoff Sutcliffe and get the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
no supp. |

Christoph Benzmüller | 44 | 28 | 25 | 24 | 18 |

Konstantin Korovin | 21 | 24 | 32 | 29 | 33 |

Hans de Nivelle | 29 | 40 | 28 | 21 | 21 |

Viorica Sofronie-Stokkermans | 44 | 38 | 24 | 17 | 16 |

No candidate reaches at least 70 first preference votes.

By redistributing the votes of Konstantin Korovin, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
no supp. |

Christoph Benzmüller | 50 | 31 | 40 | 18 |

Hans de Nivelle | 33 | 55 | 30 | 21 |

Viorica Sofronie-Stokkermans | 53 | 39 | 31 | 16 |

No candidate reaches at least 70 first preference votes.

By redistributing the votes of Hans de Nivelle, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
no supp. |

Christoph Benzmüller | 60 | 61 | 18 |

Viorica Sofronie-Stokkermans | 73 | 50 | 16 |

Now, Viorica Sofronie-Stokkermans reaches at least 70 first preference votes, and is elected.

To summarize, the 2 candidates elected are Geoff Sutcliffe and Viorica Sofronie-Stokkermans.

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

- Franz Baader (elected 2010, president)
- Amy Felty (reelected 2010)
- Martin Giese (Secretary)
- Rajeev Goré (elected 2009)
- Bernhard Gramlich (IJCAR 2012 program co-chair)
- Neil Murray (Treasurer)
- Larry Paulson (elected 2010)
- Brigitte Pientka (elected 2010)
- Renate Schmidt (elected 2009, vice president)
- Viorica Sofronie-Stokkermans (elected 2011)
- Geoff Sutcliffe (elected 2011)
- Christoph Weidenbach (elected 2009)

On behalf of the AAR and CADE Inc., I thank Christoph Benzmüller, Nikolaj Bjørner, and Reiner Hähnle for their service as trustee during the past years, and all candidates for running in the election, all the members who voted; and offer congratulations to Viorica Sofronie-Stokkermans and Geoff Sutcliffe on being elected.

Also on behalf of the AAR and CADE Inc., I thank especially Reiner Hähnle for his service as vice-president of CADE during the past six years.

After the trustee elections, the board of trustees has elected Renate Schmidt as the new vice president. I congratulate her on this, and wish her a successful term of office.