# ASSOCIATION FOR AUTOMATED REASONING

## From the AAR President, Larry Wos...

As I've indicated several times in past newsletters, simpler proofs are often important.

In logic, in particular, simpler proofs can enable one to avoid using certain terms or lemmas previously thought to be indispensable. For example, my colleague Brandon Fitelson and I were able to show that terms of the form `n(n(t))`, where `n` denotes negation, though omnipresent in the literature, are not always indispensable (Fitelson and Wos, "Missing Proofs Found," J. Automated Reasoning, vol. 27, 2000, pp. 201-225). More impressive, M. Beeson, R. Veroff, and I (mostly them) provided conditions that, if satisfied, guarantee that a double-negation proof can always be found; (M. Beeson, R. Veroff, and L. Wos, "Double-Negation Elimination in Some Propositional Logics", Studia Logica, special issue on Negation in Constructive Logic).

The same is true in algebra. For example, I have found proofs in lattice theory that rely solely on forward reasoning (through paramodulation) and are free of any use of demodulation.

A different kind of "improvement" can be illustrated in the study of Moufang loops. This area of algebra can be axiomatized with any of four identities, the following:

Axiom, Moufang 1:
`(x * y) * (z * x) = (x * (y * z)) * x.`

Axiom, Moufang 2:
`x * (y * (x * z)) = ((x * y) * x) * z.`

Axiom, Moufang 3:
`x * (y * (x * z)) = ((x * y) * x) * z.`

Axiom, Moufang 4:
`x * ((y * z) * x) = (x * y) * (z * x).`

In the mid-1990s, in answer to an open question from the 1960's, I succeeded in finding what I called a "circle of pure proofs" such that 1 implies 2, 2 implies 3, 3 implies 4, and 4 implies 1. What makes the proofs "pure" is that, for example, the proof of 1 implies 2 does not rely on 3 or 4. That proof had 23 steps. Recently, I found a far shorter proof, one of only 15 steps; this work will be reported in a notebook that will be posted shortly on my website www.automatedreasoning.net.

And here is a challenge for AAR newsletter readers: Can you find a different ordering -- perhaps by writing a simple computer program or perhaps by formulating an ingenious new methodology?

Many years ago I used OTTER to find a circle of proofs in equivalential calculus. Shortly thereafter, my colleague Bob Veroff wrote a program that found all kinds of circles of proofs in that area.

I confess that I simply do not know whether many orderings or even just one other ordering exists in Moufang loops. But I do have a warning for those of you who would like to try to find one. Algebra offers a sharp contrast to logic.

I know that I have often claimed that one need not be an expert in a particular field when attacking a problem with an automated reasoning program. Indeed, I have used W. McCune's automated reasoning program OTTER to address challenges in various types of logic and algebra with which I have only limited familiarity. If you are familiar with logic, you know that equality is often not present. In algebra, however, equality is often dominant; and its presence when using an automated reasoning program is far more complicated than one might expect. One subtlety stems from the use of the inference rule paramodulation, which is term-oriented, rather than literal-oriented, and is therefore more fecund.

This is not meant to discourage you. I continue to find such subtleties fascinating, and I invite you to participate in the excitement of attacking questions like that posed here.

## Conferences

### FLoC 2010, the Federated Logic Conference

In 2010, FLoC, the Federated Logic Conference, will be held in Edinburgh, Scotland, on 9–24 July.

The constituent meetings of FLoC 2010 include

• CAV, the Conference on Computer Aided Verification
• CSF, the IEEE Computer Security Foundations Symposium
• ICLP, the Intl. Conference on Logic Programming
• IJCAR, the Intl. Joint Conference on Automated Reasoning
• ITP, the Conference on Interactive Theorem Proving
• LICS, the IEEE Symposium on Logic In Computer Science
• RTA, the conference on Rewriting Techniques and Applications
• SAT, the conference on Theory and Applications of Satisfiability Testing

These are supplemented by numerous workshops.

The conference website gives complete details about all constituent events, but we give some more information about some of the events most relevant to the AAR community in the following...

### IJCAR 2010, International Joint Conference on Automated Reasoning

IJCAR 2010 will take place in Edinburgh, Scotland, as part of FLoC on July 16-19, 2010.

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 2010 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 2010 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 2010 will be published by Springer-Verlag in the LNAI/LNCS series.

Important dates:

• Abstract submission deadline: January 15, 2010
• Paper submission deadline: January 22, 2010
• Notification of paper decisions: March 15, 2010
• Final version of papers due: April 19, 2010

Full details are available on the IJCAR website.

### ITP 2010, Interactive Theorem Proving

ITP 2010 will take place in Edinburgh, Scotland, as part of FLoC on July 11-14, 2010.

ITP is an international conference on Interactive Theorem Proving and related issues including applications, case studies, foundations, languages, and implementations. It is a combination of TPHOLs (Theorem Proving in Higher Order Logics) and the ACL2 Workshop series. ITP 2010 is the 23rd meeting in the TPHOLs series and the 9th meeting in the ACL2 Workshop series.

Important dates:

• Abstract submission deadline: January 15, 2010
• Paper submission deadline: January 22, 2010
• Notification of paper decisions: March 15, 2010
• Final version of papers due: April 9, 2010

Full details are available on the ITP website.

### LICS 2010, Logic In Computer Science

LICS 2010 will take place in Edinburgh, Scotland, as part of FLoC on July 11–14, 2010.

LICS is an annual international forum on topics that lie at the intersection of computer science and mathematical logic.

Important Dates:

• Titles & Short Abstracts Due: January 10, 2010
• Extended Abstracts Due: January 17, 2010
• Author Notification: March 21, 2010
• Camera-ready Papers Due: April 29, 2010.

Full details are available on the LICS website.

### RTA 2010, Rewriting Techniques and Applications

RTA 2010 will take place in Edinburgh, Scotland, as part of FLoC on July 11–13.

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 15, 2010
• Paper submission January 22, 2010
• Final version: April 3, 2010

Full details are available on the RTA website.

### LPAR-16, Logic for Programming, Artificial Intelligence, and Reasoning

LPAR-16 has recently been announced to take place in Dakar, Senegal, on April 25–May 1, 2010. Check the conference web site for up to date information on this event.

## Workshops

### ARSPA-WITS'10, Automated Reasoning for Security Protocol Analysis

The ARSPA-WITS'10 workshop will be held in Paphos, Cyprus, as part of ETAPS 2010, on March 27–28. The workshop solicits submissions of papers both on mature work and on work in progress on topics including, but not limited to:

Automated reasoning techniques, Composition issues, Formal specification, Foundations of verification, Information flow analysis, Language-based security, Logic-based design, Program transformation, Security models, Static analysis, Statistical methods, Tools, Trust management

for

Access and resource usage control, Authentication, Availability and denial of service, Covert channels, Confidentiality, Integrity and privacy, Intrusion detection, Malicious code, Mobile code, Mutual distrust, Privacy, Security policies, Security protocols

Post-procedings containing high-quality submissions will be published in Springer's LNCS series.

Important dates:

• Abstract due: December 5, 2009
• Papers due: December 13, 2009
• Author Notification: January 21, 2010
• Pre-proceedings version: February 9, 2010
• Final papers: April 10, 2010

See the workshop website for details, including the full call for papers and submission instructions.

## Special Issues

### Special Issue of the Journal of Visual Languages and Computing on Visual Languages and Logic

Diagrams of one sort or another have always been used as aids to abstract reasoning. Although many are informal mnemonics, reminding their authors about structures and relationships they have observed or deduced, considerable research effort has been expended on formalising graphical notations so that they may play a more central role in the application of logic to problems.

While early work concentrated on diagrammatic representations of logic as a more intuitive or revealing paper-based replacement for textually represented logic, research in this area now mostly involves notations specifically designed for computer implementation either as computational models or interface languages. Examples include relational and existential graphs (C.S. Peirce), conceptual graphs (J.F. Sowa), various flavours of semantic networks such as conceptual dependency graphs (R. Schank), graphical deduction systems such as clause interconnectivity graphs (S. Sickel), Venn diagrams, Euler diagrams, constraint diagrams, and visual logic programming languages.

Following the success of the Workshop on Visual Languages and Logic held in 2007 and again in September 2009 (VLL 2009) (see the web page), we are soliciting, for a Special Issue of JVLC, papers in which the primary focus is research at the intersection of logic and visual languages. In particular, we invite VLL 2009 authors to submit updated and expanded versions of their papers. We expect this special issue to appear in appear in late 2010 or early 2011. Topics of interest include, but are not limited to:

• Graphical notations for logics (either classical or non-classical, such as first or higher order logic, temporal logic, description logic, independence friendly logic, spatial logic)
• Diagrammatic reasoning
• Theorem proving
• Formalisation (syntax, semantics, reasoning rules)
• Expressiveness of visual logics
• Visual logic programming languages
• Visual specification languages
• Applications
• Tool support for visual logics

If you intend to submit a paper, please email a title, abstract and keywords to a `VLL@cs.dal.ca` by November 30, 2009. This information will be used to assign referees in advance of the paper deadline.

Your paper should be emailed as a PDF to `VLL@cs.dal.ca` by January 31, 2009. Note that although PDF is not the required format for the final copies of accepted papers, it is the most convenient for reviewing.

If you have any questions about this Special Issue, please email `VLL@cs.dal.ca.`

Guest Editors:
Philip Cox, Dalhousie University
Andrew Fish and John Howse, University of Brighton

## Positions

### PhD positions at RISC, Austria

The Research Institute for Symbolic Computation, RISC, in Hagenberg, Austria, seeks applications for PhD positions. Experience in symbolic computation is advantageous but no formal requirement. Automated Reasoning and Formal Methods are amongst the topics of interest to RISC. Students who would like to start their studies in October 2010 should apply by February 15, 2010.

See here for details about these positions.

## Results of the CADE Trustee Elections

Wolfgang Ahrendt
E-mail: ahrendt@chalmers.se

An election was held from October 23 through November 13 to fill three positions on the board of trustees of CADE Inc. Rajeev Goré, Konstantin Korovin, Christopher Lynch, Brigitte Pientka, Renate Schmidt, Aaron Stump, and Christoph Weidenbach were nominated for these positions. (See AAR Newsletter No. 85, September 2009.)

Ballots were sent by electronic mail to all members of AAR on October 23, for a total of 793 ballots. Of these, 145 were returned with a vote, representing a participation level of 18.3% (as compared to 18% in 2008, 16.4% in 2007, 16.0% in 2006, 18.1% in 2005 and 19.8% in 2004 and 2003). All votes were valid. Therefore, in each iteration of the STV algorithm (as described in the CADE Bylaws, see here), a candidate is elected iff she or he gets strictly more than 72 1st preference votes. Otherwise, the votes of the candidate 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. 6th pref. 7th pref. Total R.Goré 34 10 12 11 5 9 64 145 K.Korovin 12 11 16 13 4 5 84 145 C.Lynch 16 19 19 20 10 6 55 145 B.Pientka 21 24 13 15 12 4 56 145 R.Schmidt 21 32 18 16 12 5 41 145 A.Stump 14 20 23 7 8 7 66 145 C.Weidenbach 27 22 23 4 10 4 55 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 34 12 16 7 11 27 38 145 C.Lynch 17 23 20 21 8 19 37 145 B.Pientka 25 20 19 14 10 25 32 145 R.Schmidt 24 34 19 16 9 14 29 145 A.Stump 15 24 21 8 6 34 37 145 C.Weidenbach 29 24 21 7 7 23 34 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of A.Stump one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 36 17 11 14 19 30 18 145 C.Lynch 19 27 27 14 11 30 17 145 B.Pientka 27 22 23 13 14 24 22 145 R.Schmidt 28 38 19 14 11 20 15 145 C.Weidenbach 34 25 19 7 16 31 13 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of C.Lynch one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 39 14 23 18 17 30 4 145 B.Pientka 33 30 17 18 13 23 11 145 R.Schmidt 34 41 24 7 13 18 8 145 C.Weidenbach 38 33 12 15 15 24 8 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of B.Pientka one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 44 19 27 16 21 16 2 145 R.Schmidt 47 46 12 8 16 11 5 145 C.Weidenbach 45 33 19 11 23 10 4 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of R.Goré one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Schmidt 68 36 4 12 13 12 0 145 C.Weidenbach 56 40 7 17 16 9 0 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of Candidate C.Weidenbach one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Schmidt 103 3 6 17 10 6 0 145

Now, R.Schmidt reaches more than 72 1st preference votes, and is elected to the board of trustees. The redistribution of her votes produces the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 37 13 14 7 10 42 22 145 K.Korovin 14 14 20 8 5 55 29 145 C.Lynch 18 25 24 16 7 32 23 145 B.Pientka 25 26 14 19 5 36 20 145 A.Stump 15 30 19 5 10 45 21 145 C.Weidenbach 36 25 11 13 5 35 20 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 38 17 12 13 21 28 16 145 C.Lynch 21 28 27 13 12 28 16 145 B.Pientka 29 23 22 14 17 28 12 145 A.Stump 17 35 15 5 30 28 15 145 C.Weidenbach 39 25 14 10 19 22 16 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of A.Stump one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 40 24 12 17 23 22 7 145 C.Lynch 24 39 23 8 23 20 8 145 B.Pientka 33 26 25 13 16 24 8 145 C.Weidenbach 45 26 13 15 22 17 7 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of Candidate C.Lynch one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 43 31 18 12 26 13 2 145 B.Pientka 42 35 20 8 21 14 5 145 C.Weidenbach 55 26 17 9 21 12 5 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of B.Pientka one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 56 33 12 17 18 9 0 145 C.Weidenbach 67 30 6 20 14 5 3 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of R.Goré one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total C.Weidenbach 96 5 11 20 7 6 0 145

Now, C.Weidenbach reaches more than 72 1st preference votes, and is elected to the board of trustees. The redistribution of his votes produces the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 43 15 10 10 32 26 9 145 K.Korovin 19 20 13 9 37 31 16 145 C.Lynch 27 30 20 12 17 25 14 145 B.Pientka 29 27 24 9 26 24 6 145 A.Stump 25 25 17 10 33 26 9 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 47 14 15 20 23 19 7 145 C.Lynch 32 35 18 12 17 20 11 145 B.Pientka 33 31 22 13 28 14 4 145 A.Stump 28 29 13 24 28 16 7 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of A.Stump one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 54 16 20 18 21 14 2 145 C.Lynch 43 36 14 10 24 13 5 145 B.Pientka 39 38 19 9 28 9 3 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of Candidate B.Pientka one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 63 25 14 14 23 6 0 145 C.Lynch 59 33 7 16 20 7 3 145

No candidate reaches more than 72 1st preference votes. By redistributing the votes of Candidate C.Lynch one gets the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total R.Goré 88 11 8 24 11 3 0 145

Now, R.Goré reaches more than 72 1st preference votes, and is elected to the board of trustees. The redistribution of his votes produces the following table:

 Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6th pref. 7th pref. Total K.Korovin 24 21 13 26 28 26 7 145 C.Lynch 39 28 18 15 21 17 7 145 B.Pientka 41 28 16 18 24 17 1 145 A.Stump 29 28 19 20 29 17 3 145

Altogether, the three candidates who are elected to the board of trustees in this election are Renate Schmidt, Christoph Weidenbach, and Rajeev Goré.

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

• Wolfgang Ahrendt (Secretary, appointed 5/2007)
• Christoph Benzmüller (elected 11/2008)
• Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004, reelected 10/2007)
• Amy Felty (Secretary 5/2004 to 5/2007, elected 10/2007)
• Rajeev Goré (elected 10/2004, elected 11/2009)
• Reiner Hähnle (Vice President, elected 10/2005, reelected 11/2008)
• Neil Murray (Treasurer)
• Renate Schmidt (CADE-22 program chair, elected 11/2009)
• Geoff Sutcliffe (elected 10/2004, reelected 10/2007)
• Andrei Voronkov (CADE-18 Program Chair, elected 10/2002, Vice President 2003, elected 10/2007)
• Christoph Weidenbach (elected 11/2009)

On behalf of the AAR and CADE Inc., I thank Franz Baader, Peter Baumgartner, and Aaron Stump 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 Renate Schmidt, Christoph Weidenbach, and Rajeev Goré on being elected.

Also on behalf of the AAR and CADE Inc., I thank in particular Franz Baader for his service as president of CADE during the past 6 years.