ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER No. 109, December 2014

From the AAR President, Larry Wos…
Search for New AAR Newsletter Editor
Results of CADE Trustee elections
Proposals Solicited for Sites for IJCAR 2016
Conferences
Counting of the Ballots of the CADE Trustee Elections

From the AAR President, Larry Wos…

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.

Search for New AAR Newsletter Editor

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

The Association for Automated Reasoning (AAR) is seeking a new AAR Newsletter Editor.

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:

announcements of relevant conferences, workshops, and summer schools,
reports on such events,
announcements of special issues of journals and magazines,
brief technical articles,
reports of experiments,
open problems,
presentations of systems,
abstracts of theses,
open letters, discussing issues of general interest in the AR community,
announcements of job opportunities,
CADE member information, e.g. concerning elections (as membership in CADE and AAR coincides).

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:

Larry Wos, President of AAR
Martin Giese, Secretary of AAR and CADE
Geoff Sutcliffe, AAR, CADE, and IJCAR webmaster
Maria Paola Bonacina, President of CADE, subcorporation of AAR
Hans Juergen Ohlbach, Vice-President of AAR
Pascal Fontaine, CADE Representative on the AAR Board
Brigitte Pientka, CADE Representative on the AAR Board

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)

Results of CADE Trustee elections

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

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

Peter Baumgartner (elected 2013)
Maria Paola Bonacina (elected 2013, president)
Amy Felty (CADE-25 programme co-chair)
Pascal Fontaine (elected 2014)
Martin Giese (secretary)
Jürgen Giesl (elected 2014)
Neil Murray (treasurer)
Larry Paulson (reelected 2013)
Brigitte Pientka (reelected 2013)
Renate Schmidt (reelected 2012, vice-president)
Geoff Sutcliffe (reelected 2014)
Christoph Weidenbach (reelected 2012)

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!

Proposals Solicited for Sites for IJCAR 2016

Deepak Kapur
IJCAR Steering Committee Chair
kapur@cs.unm.edu

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:

National, regional, and local AR community support:IJCAR Conference Chair and host institution, IJCAR Local Arrangements Committee, availability of (and reward for) student-volunteers.
National, regional, and local government and industry support, both organizational and financial
Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls).
An estimate on registration for the conference and workshops, both for regular and students.
Conference and exhibit facilities for the anticipated number of registrants (typically up to 200), for example, number, capacity and audiovisual equipment of meeting rooms; a large plenary session room that can hold all the registrants; enough rooms for parallel sessions/workshops/tutorials; Internet connectivity and workstations for demos/competitions; catering services; and presence of professional staff.
Residence accommodations and food services in a range of price categories and close to the conference facilities, for example, number and cost range of hotels, and availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer.
Rough budget projections for the various budget categories, e.g., cost of renting/cleaning the meeting rooms, if applicable; cost of professional conference secretariat, if hired; and financial model for satellite workshops and/or co-located events.
Balance with regard to the geographical distribution of previous IJCAR and its constituent meetings.

Perspective organizers are encouraged to get in touch with the IJCAR Steering Committee Chair for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.

Conferences

CADE-25, Conference on Automated Deduction

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.

Logics of interest include: propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, constructive, other non-classical, meta-logics, logical frameworks, type theory, set theory, as well as any combination thereof.
Paradigms of interest include: theorem proving, model building, constraint solving, computer algebra, model checking, proof checking, and their integration.
Methods of interest include: resolution, superposition, completion, saturation, term rewriting, decision procedures, model elimination, connection methods, tableaux, sequent calculi, natural deduction, as well as their supporting algorithms and data structures, including matching, unification, orderings, induction, indexing techniques, proof presentation and explanation, proof planning.
Applications of interest include: program analysis, verification and synthesis of software and hardware, formal methods, computational logic, computer mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, declarative programming, robotics, planning, and other areas of AI.

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.

RTA 2015, Rewriting Techniques and Applications

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.

CAV 2015, Computer Aided Verification

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.

TAP 2015, Tests And Proofs

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.

CICM 2015, Intelligent Computer Mathematics

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.

Counting of the Ballots of the CADE Trustee Elections

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