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):
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:
CADE's/IJCAR's near location future will be as follows:
The deadline for proposals is:
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:
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.
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
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
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.
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:
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)