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