Whether you be a tyro or a titan, the column of mine in the September 2014 AAR newsletter may have piqued your interest because of its presentation of a charming set of mathematical varieties. As noted there, these varieties move from the more familiar to the less familiar: Boolean algebra, modular ortholattices, orthomodular lattices, ortholattices, complemented lattices, lattice theory, and quasilattice theory. In that September column, the focus was on Boolean algebra; and rather than relying on meet (union), join (intersection), and complement, you were asked to work with the Sheffer stroke -- with the nand (the not of and).
Here the Sheffer stroke again comes into play. The variety of mathematics featured in this column, however, is modular ortholattices (MOL). My interest in modular ortholattices resulted, as was so often the case, from research of William McCune, the author of OTTER. Indeed, he found the following “nice” single axiom for MOL, which is the focus of your first challenge.
f(f(f(f(y,x),f(z,x)),u),f(x,f(f(f(f(f(f(y,y),x),z),z),x),y))) = x.
The challenge for you is to prove that this equation (in the Sheffer stroke, denoted by the function f
) is in fact a single axiom. As a target, I offer you a well-known 4-basis, whose denial is the following.
f(A,f(A,A)) != f(B,f(B,B)) | f(f(A,A),f(A,B)) != A | f(A,f(f(B,C),f(B,C))) != f(C,f(f(B,A),f(B,A))) | f(A,f(B,f(A,f(C,C)))) != f(A,f(C,f(A,f(B,B)))) | $Ans(modular_ortholattice).
You might prefer to see the 4-basis with its names.
f(x,f(x,x)) = f(y,f(y,y)). % one f(f(x,x),f(x,y)) = x. % absorption f(x,f(f(y,z),f(y,z))) = f(z,f(f(y,x),f(y,x))). % associativity f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). % modularity
Of course, as many of you have already surmised, the challenge has a so-called second half, namely, you are to find a proof that is forward and free of demodulation. (I strongly suspect that some of you will begin with a Knuth-Bendix approach.)
Now, I fully believe that two pieces of chocolate (unadulterated) are better than one. So I am willing to assume that you are waiting for another tasty treat, another challenge. I therefore turn again to history.
Robert Veroff, when offered four equations from McCune as candidates for being a single axiom, set to work. What made these candidates so interesting is that each has length 25, in contrast to McCune's success with the cited 27-letter single axiom for MOL. Veroff, using his approach of sketches, found the following single axiom, a 25-letter axiom for MOL; for his proof, I believe he also used the given basis as a target.
f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x.
For your second challenge, you are asked to prove that this 25-letter formula is a single axiom for MOL. Further, you are asked to then find a forward demodulation-free proof.
I believe the following observation merits inclusion. The proof that I have for this 25-letter single axiom is substantially longer than my proof for the 27-letter single axiom. But, you might assert, such should be expected; after all, a 25-letter single axiom is in several ways more appealing than a 27-letter single axiom, and some price must be paid.
I note that other members of the Argonne group years ago proved that no single axiom can be found of length 19 or less. So, taking things into consideration, you have an open question to study. Does there exist a single axiom of length 21 or 23?
I may have overlooked some recent success, and therefore perhaps this question has in fact been answered. If so, I would appreciate your letting me know about it.
Just in case, or as a bonus, I offer one more open (I believe) question: How long is the shortest single axiom for MOL in terms of join and complement? Padmanahban and Quackenbush have found, with an algorithm, single axioms for MOL in terms of join and complement, but the length of those axioms is not particularly appealing.
The AAR publishes an electronic newsletter, sent to all members, with a frequency of four times a year. The AAR newsletter is the major information channel for the automated reasoning community. Among other things, it can contain:
Earlier issues of the AAR newsletter can be found at http://www.aarinc.org/.
The role of the newsletter editor is to collect and select information for inclusion in the newsletter, to solicit contributions, to technically edit the letter as a webpage, and to send around an announcement with link and summary. All this is done in close collaboration with the following people and roles:
Acting as the AAR newsletter editor is an excellent opportunity for a deep and visible involvement in the AR community, as the role connects to all kinds of AR activities. The newsletter is a cornerstone for the community identity and development.
If you are interested in taking up this role, please reply to
Martin Giese, secretary of AAR (secretary (at) aarinc (dot) org), until
16 January 2015. Please include (links to) information about your
connection to automated reasoning. A decision will be taken by the
boards of AAR and CADE.
Looking forward to hearing from you,
Martin Giese
(Secretary of AAR and CADE)
An election was held from 10 October to 5 November to fill three positions on the board of trustees of Cade, Inc. Pascal Fontaine, Jürgen Giesl, Konstantin Korovin, Christopher Lynch, Stephan Schulz, Viorica Sofronie-Stokkermans, and Geoff Sutcliffe were nominated.
Ballots were sent by electronic mail to all members of AAR on 10 October, for a total of 1056 ballots. 106 valid ballots were returned, which translates to a participation level of 10% (as compared to 11.8% in 2013, 13,0% in 2012, 16.2% in 2011, 13.3% in 2010, 18.3% in 2009, and 18% in 2008).
The counting of the votes according to the single transferrable vote algorithm described in the CADE Bylaws is detailed at the end of this newsletter.
The three candidates elected are Geoff Sutcliffe, Pascal Fontaine, and Jürgen Giesl.
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 Viorica Sofronie-Stokkermans for her service on the CADE board of trustees for the last three years. We are also grateful to Deepak Kapur, who was an ex-officio member of the board in his function as IJCAR 2014 programme co-chair.
I further thank all candidates for running in the election, and all members who voted.
Congratulations to Geoff Sutcliffe, Pascal Fontaine, and Jürgen Giesl on being elected!
We invite proposals for sites around the world to host the 8th International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2016. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; IJCAR 2006 as part of FLoC in Seattle, Washington; IJCAR 2008 in Sydney, Australia; IJCAR 2010 in Edinburgh, Scotland, as part of FLoC, IJCAR 2012 in Manchester, UK, and IJCAR 2014 in Vienna, Austria, as part of Vienna Summer of Logic.
The IJCAR is a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), and FroCoS (Workshop on Frontiers of Combining Systems) and possibly other meetings. The 14th SMT workshop will be co-located with IJCAR 2016; many other workshops are also expected to be affiliated with the conference.
The deadline for proposals is January 31, 2015. Proposals should be sent to the IJCAR Steering Committee Chair (see contact information above). We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
The 25th International Conference on Automated Deduction will be held in Berlin, Germany, 1–7 August 2015.
CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference invites high-quality submissions on the general topic of automated reasoning, including foundations, applications, implementations and practical experiences.
The CADE program will include the annual CADE ATP System Competition (CASC), as well as various workshops and tutorials. Details will be published in separate calls and on the conference website.
CADE calls for regular papers of up to 15 pages and system descriptions of up to 10 pages.
Papers shall be submitted until 23 February 2015. An abstract must be submitted already on 16 February 2015. Accepted papers will be published in Springer's LNCS series.
Please refer to the conference web site for further information, including the full Call for Papers.
The 26th International Conference on Rewriting Techniques and Applications will be held in Warsaw, Poland on 29 June–1 July 2015.RTA is the major forum for the presentation of research on all aspects of rewriting.
The deadline for title and abstract submissions is on 30 January 2015, and full papers are due on 6 February 2015.
Full details are available on the website.
The 27th International Conference on Computer Aided Verification, CAV 2015, will be held in San Francisco, California, USA, on 18–24 July 2015. The CAV conference series is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems.
Abstract submission closes on 30 January 2015, full papers are to be submitted by 6 February 2015.
Refer to the CAV website for further information.
The 9th International Conference on Tests and Proofs, TAP 2015, will take place in L'Aquila, Italy, on 20–24 July 2015, as part of STAF 2015,
The TAP conference is devoted to the synergy of proofs and tests, to the application of techniques from both sides and their combination for the advancement of software quality.
Research papers of up to 16 pages, and short papers of up to 6 pages should be submitted until 20 February 2015, abstracts are due on 13 February. TAP also invites tutorial proposals.
For detailed information, see the conference web site.
The Conference on Intelligent Computer Mathematics, CICM 2015, will be held in Washington DC, USA, on 13–17 July 2015.
Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. CICM offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas.
Submission of abstracts is due on 16 February 2015, with full papers due on 23 February.
For further details, please refer to the conference website.
106 valid ballots were returned. Therefore, in each iteration of the single transferrable vote algorithm described in the CADE Bylaws, a candidate is elected if she or he gets at least 54 first preference votes. Otherwise, the votes of the candidate with the least first 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. | no supp. |
Pascal Fontaine | 27 | 12 | 13 | 12 | 9 | 5 | 6 | 22 |
Jürgen Giesl | 17 | 16 | 17 | 14 | 13 | 9 | 3 | 17 |
Konstantin Korovin | 4 | 11 | 15 | 14 | 14 | 10 | 11 | 27 |
Christopher Lynch | 5 | 12 | 13 | 9 | 10 | 12 | 20 | 25 |
Stephan Schulz | 14 | 17 | 12 | 13 | 14 | 14 | 9 | 13 |
Viorica Sofronie-Stokkermans | 13 | 11 | 20 | 14 | 8 | 12 | 8 | 20 |
Geoff Sutcliffe | 26 | 25 | 13 | 11 | 10 | 5 | 5 | 11 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Konstantin Korovin, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | 6th pref. | no supp. |
Pascal Fontaine | 28 | 15 | 13 | 14 | 6 | 8 | 22 |
Jürgen Giesl | 18 | 15 | 22 | 19 | 11 | 4 | 17 |
Christopher Lynch | 5 | 14 | 14 | 11 | 12 | 25 | 25 |
Stephan Schulz | 15 | 17 | 14 | 18 | 18 | 11 | 13 |
Viorica Sofronie-Stokkermans | 13 | 15 | 26 | 5 | 18 | 9 | 20 |
Geoff Sutcliffe | 27 | 27 | 11 | 16 | 8 | 6 | 11 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Christopher Lynch, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | no supp. |
Pascal Fontaine | 28 | 19 | 13 | 13 | 11 | 22 |
Jürgen Giesl | 19 | 18 | 27 | 14 | 11 | 17 |
Stephan Schulz | 15 | 19 | 22 | 17 | 19 | 14 |
Viorica Sofronie-Stokkermans | 14 | 21 | 19 | 17 | 15 | 20 |
Geoff Sutcliffe | 30 | 26 | 14 | 16 | 9 | 11 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Viorica Sofronie-Stokkermans, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
Pascal Fontaine | 31 | 21 | 17 | 15 | 22 |
Jürgen Giesl | 23 | 29 | 20 | 17 | 17 |
Stephan Schulz | 17 | 22 | 30 | 23 | 14 |
Geoff Sutcliffe | 33 | 28 | 22 | 12 | 11 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Stephan Schulz, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
Pascal Fontaine | 32 | 34 | 18 | 22 |
Jürgen Giesl | 29 | 33 | 26 | 18 |
Geoff Sutcliffe | 43 | 27 | 25 | 11 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Jürgen Giesl, one gets the following table:
Candidate | 1st pref. | 2nd pref. | no supp. |
Pascal Fontaine | 47 | 37 | 22 |
Geoff Sutcliffe | 56 | 38 | 12 |
Now, Geoff Sutcliffe reaches at least 54 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. | 5th pref. | 6th pref. | no supp. |
Pascal Fontaine | 30 | 19 | 10 | 12 | 6 | 7 | 22 |
Jürgen Giesl | 19 | 25 | 15 | 16 | 11 | 3 | 17 |
Konstantin Korovin | 7 | 17 | 15 | 17 | 12 | 11 | 27 |
Christopher Lynch | 10 | 12 | 14 | 11 | 14 | 20 | 25 |
Stephan Schulz | 23 | 15 | 15 | 12 | 17 | 11 | 13 |
Viorica Sofronie-Stokkermans | 17 | 15 | 22 | 12 | 9 | 11 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Konstantin Korovin, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | no supp. |
Pascal Fontaine | 33 | 20 | 13 | 8 | 10 | 22 |
Jürgen Giesl | 20 | 27 | 22 | 16 | 4 | 17 |
Christopher Lynch | 11 | 13 | 17 | 15 | 25 | 25 |
Stephan Schulz | 25 | 15 | 17 | 23 | 13 | 13 |
Viorica Sofronie-Stokkermans | 17 | 25 | 17 | 15 | 12 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Christopher Lynch, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | no supp. |
Pascal Fontaine | 35 | 22 | 12 | 15 | 22 |
Jürgen Giesl | 24 | 28 | 26 | 11 | 17 |
Stephan Schulz | 26 | 21 | 21 | 24 | 14 |
Viorica Sofronie-Stokkermans | 21 | 25 | 22 | 18 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Viorica Sofronie-Stokkermans, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
Pascal Fontaine | 41 | 23 | 20 | 22 |
Jürgen Giesl | 33 | 37 | 19 | 17 |
Stephan Schulz | 29 | 30 | 33 | 14 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Stephan Schulz, one gets the following table:
Candidate | 1st pref. | 2nd pref. | no supp. |
Pascal Fontaine | 51 | 33 | 22 |
Jürgen Giesl | 47 | 41 | 18 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Jürgen Giesl, one gets the following table:
Candidate | 1st pref. | no supp. |
Pascal Fontaine | 84 | 22 |
Now, Pascal Fontaine reaches at least 54 first preference votes, and is elected.
To find the next elected candidate, we redistribute the votes of Pascal Fontaine and get the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | 4th pref. | 5th pref. | no supp. |
Jürgen Giesl | 26 | 27 | 19 | 13 | 4 | 17 |
Konstantin Korovin | 11 | 27 | 10 | 17 | 14 | 27 |
Christopher Lynch | 15 | 11 | 18 | 16 | 21 | 25 |
Stephan Schulz | 30 | 15 | 19 | 15 | 14 | 13 |
Viorica Sofronie-Stokkermans | 23 | 21 | 18 | 13 | 11 | 20 |
No candidate reaches at least 54 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. |
Jürgen Giesl | 28 | 35 | 20 | 6 | 17 |
Christopher Lynch | 16 | 17 | 19 | 29 | 25 |
Stephan Schulz | 34 | 15 | 27 | 17 | 13 |
Viorica Sofronie-Stokkermans | 27 | 27 | 17 | 15 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Christopher Lynch, one gets the following table:
Candidate | 1st pref. | 2nd pref. | 3rd pref. | no supp. |
Jürgen Giesl | 34 | 39 | 16 | 17 |
Stephan Schulz | 38 | 22 | 32 | 14 |
Viorica Sofronie-Stokkermans | 33 | 29 | 24 | 20 |
No candidate reaches at least 54 first preference votes.
By redistributing the votes of Viorica Sofronie-Stokkermans, one gets the following table:
Candidate | 1st pref. | 2nd pref. | no supp. |
Jürgen Giesl | 56 | 33 | 17 |
Stephan Schulz | 45 | 47 | 14 |
Now, Jürgen Giesl reaches at least 54 first preference votes, and is elected.
To summarize, the three candidates elected are Geoff Sutcliffe, Pascal Fontaine, and Jürgen Giesl.