ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 94, December 2011

From the AAR President, Larry Wos...

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.

A Note on Identities in Groups and Semigroups

Sherman Stein
Prof. Emer. Math. UCDavis
E-mail: stein (at) math.ucdavis.edu

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.

Conferences

IJCAR 2012, International Joint Conference on Automated Reasoning

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:

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:

Full details are available on the IJCAR website.

NFM 2012, NASA Formal Methods Symposium

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, Rewriting Techniques and Applications

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:

Full details are available on the RTA website.

ITP 2012: Interactive Theorem Proving

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:

Full details are available on the conference web site.

WoLLIC 2012, Workshop on Logic, Language, Information and Computation

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.

Workshops

IWIL-2012, Intl. Workshop on the Implementation of Logics

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, Analytic Proof Systems

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.

Winter School on Verification

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:

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

  1. A letter of motivation,
  2. a transcript of courses and grades with a translation into English by the applicant, and
  3. 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, a financial service for communities

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

Call for Papers: “Automated Reasoning and Mathematics: Essays in Memory of William McCune”

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:

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

RISC ProgramExplorer 1.0

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.

Results of CADE Elections

Martin Giese
(Secretary of AAR and CADE)
E-mail: martingi (at) ifi.uio.no

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

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.