NEWSLETTER No. 84, July 2009

- From the AAR President, Larry Wos...
- Herbrand Award
- Call for Nominations: CADE Trustees Election
- Proposals for sites for CADE-23 in 2011 solicited
- A Note on LEO-II and the Basic Fragment of Simple Type Theory
- Conferences
- Special Issues

I am an optimist. But even I was surprised and delighted at the response I received to my previous President's Column, in which I offered two possible new single axioms for an area of logic known as BCI. My goal was obvious: to provide material for research and for enjoyment. Within less than two days after the column was published, the questions raised in that column were answered.

The two formulas offered for consideration were the following.

P(i(u,i(i(v,w),i(i(i(x,x),i(y,i(u,v))),i(y,w))))). % BCI-Candidate 42 P(i(i(i(i(i(u,u),i(v,w)),i(i(x,v),w)),y),i(x,y))). % BCI-Candidate 46

The first was conjectured to be too weak, and the second more promising.

As it turned out, each has been proved to be a new single axiom for BCI. The first, candidate 42, was proved to be a single axiom by Mark Stickel with his powerful program SNARK. The second was proved (by me) to be a single axiom with OTTER. And, no, I did not cheat: I did not have that proof in hand when the column appeared.

Further—so marvelous!—those results were shared by various researchers, with the result that many other new single axioms were found, many by the logician D. Ulrich, some by Mark Stickel, and some by John Halleck.

The evidence is in: The AAR newsletter can and sometimes does advance areas of logic and mathematics. And now, to continue the momentum, I invite you to provide similar challenges for AAR newsletter readers.

It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Deepak Kapur is to receive the 2009 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of of his seminal contributions to several areas of automated deduction including inductive theorem proving, geometry theorem proving, term rewriting, unification theory, integration and combination of decision procedures, lemma and loop invariant generation, as well as his work in computer algebra, which helped to bridge the gap between the two areas.

The award will be presented to Professor Kapur at the 22nd International Conference on Automated Deduction (CADE-22) in Montreal, Canada.

*Franz Baader
President of CADE Inc.*

*by Wolfgang Ahrendt, Secretary of AAR and CADE*

Nominations for two CADE trustee positions are being sought, in preparation for the elections to be held after CADE 2009.

The members of the board of trustees are (in alphabetical order):

- Wolfgang Ahrendt (Secretary)
- Franz Baader (President, elected 2003, reelected 2006)
- Peter Baumgartner (elected 2003, reelected 2006)
- Christoph Benzmueller (elected 2008)
- Maria Paola Bonacina (elected 2004, reelected 2007)
- Amy Felty (elected 2007)
- Juergen Giesl (IJCAR 2010 Program Co-chair)
- Reiner Haehnle (Vice President, elected 2005, reelected 2008)
- Neil Murray (Treasurer)
- Renate A. Schmidt (CADE 2009 Program Chair)
- Geoff Sutcliffe (elected 2004, reelected 2007)
- Aaron Stump (elected 2006)
- Andrei Voronkov (elected 2007)

The terms of Franz Baader, Peter Baumgartner, and Aaron Stump expire. Aaron Stump is eligible to be nominated for a second term. Franz Baader and Peter Baumgartner have served two successive elected terms, and are therefore not eligible to be nominated again.

The term of office of Renate A. Schmidt as CADE 2009 program chair also ends. As outgoing ex-officio trustee, she is eligible to be nominated as an elected trustee.

Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at CADE 2009. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE Web site.

E-mail nominations are to be sent to Franz Baader, CADE President
(`baader (at) tcs.inf.tu-dresden.de`

) and Wolfgang Ahrendt,
CADE Secretary (`ahrendt (at) chalmers.se`

), up to the
upcoming CADE business meeting (to be held on 4th of August, at CADE
2009), or otherwise during the CADE business meeting.

We invite proposals for sites around the world to host the Conference on Automated Deduction (CADE) to be held in summer 2011 as a stand-alone conference. In some other years, CADE is held as part of FLoC and sometimes merges with other automated reasoning conferences into IJCAR. CADE's/IJCAR's recent location history is as follows:

- 2000: CADE-17 in North America
- 2001: IJCAR 2001 in Europe
- 2002: CADE-18 as part of FLoC in Europe
- 2003: CADE-19 in North America
- 2004: IJCAR 2004 in Europe
- 2005: CADE-20 in Europe
- 2006: IJCAR 2006 as part of FLoC in North America
- 2007: CADE-21 in Europe
- 2008: IJCAR 2008 in Australia
- 2009: CADE-22 in North America

CADE's/IJCAR's near location future will be as follows:

- 2010: IJCAR 2010 as part of FLoC in Europe

The deadline for proposals is:

September 30, 2009

In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.

Proposals should address the following points that also represent criteria for evaluation:

- National, regional, and local AR community support:
- CADE Conference Chair and host institution,
- CADE 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).
- Conference and exhibit facilities for the anticipated number
of registrants (typically 100-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,
- 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,
- 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,
- financial model for satellite workshops and/or co-located events.

- Balance with regard to the geographical distribution of previous conferences.

Perspective organizers are encouraged to get in touch with the CADE secretary and president (see contact information below) 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.

*Franz Baader, CADE President
baader (at) tcs.inf.tu-dresden.de*

*Wolfgang Ahrendt, CADE Secretary
ahrendt (at) chalmers.se*

*Christoph Benzmüller
International University in Germany, Bruchsal, Germany and Articulate Software, CA, U.S.*

LEO-II can now prove some challenge problems in the basic fragment of simple type theory.

Brown and Smolka [BS09b] present five very useful challenge problems in the basic fragment of simple type theory (the types of the constants are as follows: h:o→i , x:o, y:o, f:o→o, g:o→o, p:(o→o)→o,q:(o→o)→(o→o))

(1) | h( h(false)=h(~false) ) =/= h(false) |

(2) | h(f(f(f x))) =/= h(f x) |

(3) | x =/= y & g x = y & g y = x & f(f(f x)) = g(f x) |

(4) | x =/= y & g x = y & g y = x & p g & ~ (p ~) |

(5) | q f x & f(f x) & f (q f x) =/= f x |

The task is to show that these statements are unsatisfiable, i.e. imply falsehood.

Another related example, that is not in the basic fragment of simple type theory, is the (negated) Kaminski equation:

(6) | f(f(f x)) =/= f x |

The TPTP THF [BRS08] encodings of these problems are available under the following links: 1, 2, 3, 4, 5, 6.

Brown and Smolka remark, that most of these formulas are out of reach for the automated tactics of Isabelle [NPW02] and the higher-order provers TPS [AB06] and LEO-II [BTPF08].

For the latest version of LEO-II (version 1.0) this comment is no
longer valid. LEO-II (`http://leoprover.org`) is a
resolution based higher-order ATP system designed to cooperate with
specialist systems for fragments of higher-order logic and proof
search in LEO-II is based on extensional higher-order (RUE-)resolution
[Ben99a,Ben99b]. This calculus shares important similarities with the
recent tableaux based calculi of Brown and Smolka for the basic
fragment of simple type theory [BS09b] and for
extended first order logic [BS09a].

The study of the above examples has led to the detection of some heuristic constraints in LEO-II's search procedure that were too restrictive. Thus, no new rules were added to LEO-II's extensional higher-order (RUE-)resolution approach, but only some heuristically motivated restrictions on rule applications were skipped in the implementation. Thereby we obtain the following results (all experiments were conducted on an iMac, Intel Core 2 Duo, 2.8 GHz, 2GB Memory):

Problem | LEO-II + E | |

(1) | h( h(false)=h(~false) ) =/= h(false) | 0.075 sec |

(2) | h(f(f(f x))) =/= h(f x) | 0.112 sec |

(3) | x =/= y & g x = y & g y = x & f(f(f x)) = g(f x) | - |

(4) | x =/= y & g x = y & g y = x & p g & ~ (p ~) | 0.155 sec |

(5) | q f x & f(f x) & f (q f x) =/= f x | 0.130 sec |

(6) | (f(f(f x))) = (f x) | 0.192 sec |

This `link` presents a proof object in TPTP TSTP format generated for Example (1)
by LEO-II when called in standalone mode, i.e. when explicitly disabling
the collaboration with prover E [Sch02]. In this case
LEO-II proves Example (1) even in 0.018 sec.
And this `link` presents a proof object for Example (2) when calling LEO-II in
standalone mode. In this case LEO-II proves Example (2) in
1.296 sec.

The problems of Brown and Smolka are relevant and interesting test problems for higher-order automated theorem provers. Except for problem (3) they are now trivial for LEO-II. For (3) a relaxation of LEO-II's highly restricted factorisation rule seems required. First tests have shown that this will likely negatively influence LEO-II's performance for other examples and therefore we have not considered this an option so far. The relaxations of heuristics that were needed to obtain the results reported in this note do not negatively influence the overall performance of LEO-II for TPTP-v3.7.0. Future work includes further adaptations of LEO-II's proof search procedure to obtain a resolution based decision procedure for the basic fragment of simple type theory.

- AB06
- P.B. Andrews and C. Brown. TPS: A Hybrid Automatic-Interactive System for Developing Proofs. Journal of Applied Logic, 4(4):367-395, 2006.
- Ben99a
- C. Benzmüller. Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Naturwissenschaftlich-Technische Fakultät I, Saarland University, Saarbrücken, Germany, 1999.
- Ben99b
- C. Benzmüller. Extensional higher-order paramodulation and RUE-resolution. CADE-16, volume 1632 in LNCS. Springer, 1999.
- BRS08
- C. Benzmüller, F. Rabe, and G. Sutcliffe, The Core TPTP Language for Classical Higher-Order Logic. IJCAR'08, volume 5195 in LNAI,Springer, 2008.
- BTPF08
- Christoph Benzmüller, Frank Theiss, Larry Paulson, and Arnaud Fietzke. LEO-II - a cooperative automatic theorem prover for higher-order logic. IJCAR'06, volume 5195 of LNAI, Springer, 2008.
- BS09a
- Chad E. Brown and Gert Smolka. Extended first-order logic. TPHOLs 2009, volume 5674 of LNCS, Springer, 2009.
- BS09b
- Chad E. Brown and Gert Smolka. Terminating tableaux for the basic fragment of simple type theory. TABLEAUX 2009, volume 5607 of LNCS, Springer, 2009.
- NPW02
- T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Volume 2283 in LNCS, Springer, 2002.
- SCH02
- S. Schulz. E: A Brainiac Theorem Prover. AI Communications, 15(2-3):111-126, 2002.

Registration is still possible for the 22nd International Conference on Automated Deduction to be held at McGill University, Montreal, Canada, August 2-7, 2009

See the conference web site for full information.

CADE is the major forum for the presentation of research in all aspects of automated deduction.

The conference features

- 3 invited talks
- 32 contributed papers of which 5 are system papers
- the presentation of the Herbrand Award to Deepak Kapur
- a two-day programme of workshops, tutorials and meetings
- 2 system competitions

- Konstantin Korovin (The University of Manchester)

*Instantiation-Based Automated Reasoning: From Theory to Practice* - Martin Rinard (Massachusetts Institute of Technology)

*Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival* - Mark Stickel (SRI International)

*Building Theorem Provers*

- Automated Deduction: Decidability, Complexity, Tractability (ADDCT) and The International Workshop on Unification (UNIF)
- Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
- Modules and Libraries for Proof Assistants (MLPA)
- Proof Search in Type Theories (PSTT)
- Satisfiability Modulo Theories (SMT)

- Hierarchical and Modular Reasoning in Complex Theories

with Viorica Sofronie-Stokkermans - Probabilistic Analysis Using a Theorem Prover

with Osman Hasan and Sofiene Tahar - Precise, Automated and Scalable Verification of Systems
Software Using SMT Solvers

with Shuvendu K. Lahiri and Shaz Qadeer - Logics with Undefinedness

with William M. Farmer

- The CADE ATP System Competition (CASC)
- Satisfiability Modulo Theories Competition (SMT-COMP)

- The 6th TPTP Tea Party

- Welcome reception at the McCord Museum of Canadian History
- Squash tournament at McGill Sports Centre
- Walking or biking tour excursion through Old Montreal
- Conference banquet at the elegant Pointe-à-Callière, Montreal's Museum of Archeology and History at the Old Port

Montreal is an bustling, cosmopolitan and affordable city with a charming Francophone culture. It is easily accessible from the US, Europe and world-wide with direct flights to Pierre Elliott Trudeau Airport (YUL) from all major cities.

On-line registration is still open here.

Please refer to the conference website for registration, accommodation, travel and visa information.

The fifth Federated Logic Conference (FLoC'10), will be 9-21 July, 2010 hosted by the University of Edinburgh. See the Conference Web Page for full details.

The following seven conferences will participate in FLoC

**International Conference on Computer-Aided Verification (CAV).**Workshop Chair: Tomas Vojnar**International Conference on Interactive Theorem Proving (ITP).**Workshop Chair: Michael Norrish.**International Conference on Logic Programming (ICLP).**Workshop Chair: Veronica Dahl.**International Joint Conference on Automated Reasoning (IJCAR).**Workshop Chair: Aaron Stump.**IEEE Symposium on Logic in Computer Science (LICS).**Workshop Co-Chairs: Adriana Compagnon and Maribel Fernandez.**International Conference on Rewriting Techniques and Applications (RTA).**Workshop Chair: Christopher A. Lynch.**International Conference on Theory and Applications of Satisfiability Testing (SAT).**Workshop Chair: Carsten Sinz

The organizers have made arrangements to facilitate the running of pre-, post-, and mid-FLoC workshops. Each workshop will have its own registration, with uniform FLoC workshop fees. It is not necessary to register for FLoC in order to attend workshops. Meeting rooms and accommodations will be reserved by the university in the center of Edinburgh.

- Pre-FLoC workshops: Friday & Saturday, July 9-10
- Mid-FLoC workshops: Wednesday & Thursday, July 14-15
- Post-FLoC workshops: Tuesday & Wednesday, July 20, 21.

Researchers and practitioners are invited to submit proposals for workshops on topics relating logic, broadly understood, applied to computer science. Each workshop proposal must indicate one sponsoring conference among the participating conferences. (It is suggested that prospective workshop organizers contact the relevant conference Workshop Chair before submitting a proposal.) Workshops will have to be financially self-supporting, unless the sponsoring conference accepts financial responsibility. The FLoC Organizing Committee will determine the final list of accepted workshops based on the recommendations from the Workshop Chairs of the sponsoring conferences and subject to the availability of space and facilities.

Detailed requirements, submission instructions, and contact information can be found on the FLoC'10 call for workshop proposals page.

The Journal of Symbolic Computation will publish a special
issue on the topic of **invariant generation** and **advanced
techniques for reasoning about loops**

Paper submission: September 1, 2009

Notification of acceptance: December 1, 2009

Submission of the final accepted version: Jan 4, 2009

Publication: First quarter of 2010

Loops and recursion remain key challenges for program verification research. While most systems concerned with program verification deal with loops by loop invariants or induction hypotheses that have to be provided by a human, a number of interesting alternative approaches have emerged. Especially promising breakthroughs are techniques based on Gröbner bases, quantifier elimination, and algorithmic combinatorics, which can be used in conjunction with model checking, theorem proving, static analysis and abstract interpretation.

This special issue is related to the topics of the workshop WING'09 Workshop on Invariant Generation, which took place as a satellite event of ETAPS 2009, in York, March 28, 2009. It will be published by Elsevier within the Journal of Symbolic Computation.

Both participants of the WING'09 workshop and other authors are invited to submit contributions.

This special issue focuses on advanced techniques for proving properties of programs with loops or recursion.

Relevant topics include (but are not limited to) the following:

- Program analysis and verification
- Inductive Assertion Generation
- Inductive Proofs for Reasoning about Loops
- Applications to Assertion Generation using the following tools:
- Abstract Interpretation,
- Static Analysis,
- Model Checking,
- Theorem Proving,
- Algebraic Techniques

- Tools for inductive assertion generation and verification
- Alternative techniques for reasoning about loops

This special issue welcomes original high-quality contributions that have been neither published in nor submitted to any journals or refereed conferences. Submissions will be peer-reviewed using the standard refereeing procedure of the Journal of Symbolic Computation.

Please prepare your submission in LaTeX using the JSC document
format from The JSC web page
and send it as a
Postscript or PDF file to `laura.kovacs (at) epfl.ch`

and `A.Ireland (at) hw.ac.uk`

!

Martin Giese (University of Oslo, Norway)

Andrew Ireland (Heriot-Watt University, UK)

Laura Kovacs (EPFL, Switzerland)