ASSOCIATION FOR AUTOMATED REASONING

• From the AAR President, Larry Wos...
• Conferences
  • FLoC 2010, the Federated Logic Conference
  • IJCAR 2010, International Joint Conference on Automated Reasoning
  • ITP 2010, Interactive Theorem Proving
  • LICS 2010, Logic In Computer Science
  • RTA 2010, Rewriting Techniques and Applications
  • LPAR-16, Logic for Programming, Artificial Intelligence, and Reasoning
• Workshops
  • ARSPA-WITS'10, Automated Reasoning for Security Protocol Analysis
• Special Issues
  • Special Issue of the Journal of Visual Languages and Computing on Visual Languages and Logic
• Positions
  • PhD positions at RISC, Austria
• Results of the CADE Trustee Elections

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
• Notification: March 8, 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
(Secretary of AAR and CADE)
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:

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

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

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

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

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

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

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:

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

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

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

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

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

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:

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

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

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

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

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:

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.