NEWSLETTER No. 83, April 2009

From the AAR President, Larry Wos...

Many areas of logic can be studied successfully with an automated reasoning program. Equivalential calculus, classical propositional calculus, and others are such. Indeed, reasoning programs have occasionally played a key role in answering open questions in logic. Here you are offered a challenge.

An automated reasoning program can sometimes be used to show that no proof exists, where the argument does not depend on finding an appropriate model. For example, in the early 1980s, certain formulas in equivalential calculus were shown to be too weak, by characterizing all of the deducible formulas from each and showing that certain theorems could, therefore, not be deduced. From the viewpoint of logic, knowing that a formula cannot serve as a single axiom is often as interesting as knowing that it can.

Let's consider the axioms of the BCI logic.

P(i(i(x,y),i(i(z,x),i(z,y)))).  % B
P(i(i(x,i(y,z)),i(y,i(x,z)))).  % C
P(i(x,x)).                      % I

Condensed detachment is a typical rule of inference used to study such systems. It is captured by the following in the presence of hyperresolution.

-P(i(x,y)) | -P(x) | P(y).  %  condensed detachment

And here is a candidate formula that I find enticing.

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

You are asked to formulate, if possible, an automated method showing that Candidate 42 is not a single axiom. It is, in fact, a theorem of BCI, but so far I have been unable to show that it is strong enough to be a single axiom. I doubt it is, my suspicion being based on the fact that, as it appears, all deducible theorems from the formula contain an alphabetic variant of i(x,x). But I would love to be proved wrong.

Here's another candidate formula presenting a challenge of a different type.

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

I've included Candidate 46 in that its use as the sole hypothesis in the BCI logic seems somewhat promising, for it leads to theorems that are interesting. Yet I have not been able to prove its status as a single axiom.

Lest you be discouraged, let me assure you that I and a few of my colleagues have played with other candidate formulas that, after considerable effort, turned out to be single axioms.

Perhaps you will prove something of interest for the forthcoming CADE-22 conference, which focuses on logics and proofs.

Results of the CADE Trustee Elections 2008

Wolfgang Ahrendt
Secretary of AAR and CADE
E-mail: ahrendt (at)

An election was held from November 4 through Noveber 25 to fill two positions on the board of trustees of CADE Inc. Alessandro Armando, Christoph Benzmüller, Reiner Hähnle, Konstantin Korovin, Brigitte Pientka, and Cesare Tinelli were nominated for these positions. (See AAR Newsletter No. 82, November 2008.)

Ballots were sent by electronic mail to all members of AAR on November 4, for a total of 773 ballots. Of these, 139 were returned with a vote, representing a participation level of 18% (as compared to 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 (the STV (Single Transferrable Vote) algorithm is described in the CADE Bylaws), a candidate is elected iff he or she gets strictly more than 69 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. 6rd pref. Total
A.Armando 20 14 20 20 12 53 139
C.Benzmüller 26 29 16 9 11 48 139
R.Hähnle 38 19 14 12 9 47 139
K.Korovin 12 17 9 7 12 82 139
B.Pientka 24 20 23 8 10 54 139
C.Tinelli 19 30 20 12 7 51 139

No candidate reaches more than 69 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. 6rd pref. Total
A.Armando 21 17 23 15 31 32 139
C.Benzmüller 31 27 15 12 27 27 139
R.Hähnle 39 20 14 16 25 25 139
B.Pientka 26 22 23 10 26 32 139
C.Tinelli 20 37 14 15 24 29 139

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

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
A.Armando 27 25 22 25 22 18 139
C.Benzmüller 37 30 16 21 22 13 139
R.Hähnle 42 25 18 20 20 14 139
B.Pientka 30 29 19 19 28 14 139

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

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
C.Benzmüller 42 33 25 16 18 5 139
R.Hähnle 50 29 22 16 12 10 139
B.Pientka 37 31 26 17 19 9 139

No candidate reaches more than 69 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. 6rd pref. Total
C.Benzmüller 54 43 10 18 13 1 139
R.Hähnle 63 35 10 15 12 4 139

No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Benzmüller one gets the following table:

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
R.Hähnle 98 1 16 15 9 0 139

Now, R.Hähnle reaches more than 69 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. 6rd pref. Total
A.Armando 23 18 26 18 32 22 139
C.Benzmüller 37 29 11 12 28 22 139
K.Korovin 15 17 13 11 58 25 139
B.Pientka 30 29 13 11 34 22 139
C.Tinelli 33 24 21 10 28 23 139

No candidate reaches more than 69 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. 6rd pref. Total
A.Armando 24 23 26 25 28 13 139
C.Benzmüller 44 24 13 19 29 10 139
B.Pientka 33 30 16 16 34 10 139
C.Tinelli 35 29 21 16 24 14 139

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

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
C.Benzmüller 48 27 23 17 21 3 139
B.Pientka 39 35 18 19 23 5 139
C.Tinelli 43 28 27 14 17 10 139

No candidate reaches more than 69 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. 6rd pref. Total
C.Benzmüller 60 37 7 22 13 0 139
C.Tinelli 58 39 6 16 16 4 139

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

Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
C.Benzmüller 97 1 19 16 6 0 139

Now, C.Benzmüller reaches more than 69 1st preference votes, and is elected to the board of trustees.

Altogether, the two candidates who are elected to the board of trustees in this election are Reiner Hähnle and Christoph Benzmüller.

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

On behalf of the AAR and CADE Inc., I thank Cesare Tinelli for his service as trustee during the past 3 years, Alessandro Armando for his service as ex-officio trustee (as IJCAR 2008 program co-chair), all candidates for running in the election, all the members who voted; and offer congratulations to Reiner Hähnle and Christoph Benzmüller on being elected.

Reiner Hähnle re-elected as CADE vice-president

Wolfgang Ahrendt
Secretary of AAR and CADE
E-mail: ahrendt (at)

The newly formed board of trustees held an election of the CADE vice-president, as the term of Reiner Hähnle as vice-president was expiring. Reiner was re-nominated, and furthermore, Maria Paola Bonacina was nominated. Out of these two, Reiner was elected. We thank Maria Paola and Reiner for running in the election, and offer congratulations to Reiner for being re-elected.

Call for Nominations for Herbrand Award

Wolfgang Ahrendt
Secretary of AAR and CADE
On behalf of the CADE Inc. Board of Trustees

The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of automated deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE 2009 is May 12, 2009.

Nominations pending from previous years must be resubmitted in order to be considered. Nominations should consist of a letter (preferably email) of up to 2,000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2,000 words of endorsement from two other seconders. Nominations should be sent to Franz Baader, president of CADE Inc. (baader (at) with copies to Wolfgang Ahrendt (ahrendt (at)

Call for Nominations: Editor-in-Chief of ACM Transactions on Computational Logic (ToCL)

Nominations (including self nominations) are invited for the next Editor-in-Chief of ACM Transactions on Computational Logic (ToCL), see here. The position is for a term (renewable once) of three years, starting on July 1, 2009.

Candidates should be well-established researchers in areas related to computational logic, broadly conceived, and should have sufficient experience serving on conference program committees and journal editorial boards. Nominations, including a current curriculum vita and a brief (one page) statement of vision for ToCL, should be sent to Joseph Halpern , by May 1, 2009.

Final selection will be made by a Selection Committee, consisting of Joseph Halpern (chair – Cornell University), Kryzsztof Apt (CWI), Prakash Panangaden (McGill University), and Gordon Plotkin (University of Edinburgh). Nominations received after May 1, 2009, will be considered up until the position is filled.

Woody Bledsoe Student Travel Awards

The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the the Conference on Automated Deduction (CADE) by covering much of their expenses. The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accommodation expenses (past awards have varied, but have typically been corresponding to CA$250 to CA$1000). Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.

The awards are sponsored by CADE Inc.

See the CADE 2009 web pages for more information, including application details. The deadline for applications is 16 June 2009.

Practical Progress in the Development of Automated Theorem Proving for Higher-order Logic

Geoff Sutcliffe** and Chris Benzmüller

with help from lots of people, particularly

Chad Brown and Frank Theiss*** and Florian Rabe,

and with honorable mention

Lucas Dixon, Stefan Berghofer, Makarius Wenzel, Jasmin Blanchette, Andrei Tchaltsev, Alexandre Riazanov.

* The research leading to these results has received funding from the European Community's Seventh Framework Programme FP7/2007-2013, under grant agreement PIIF-GA-2008-219982.
** Most of the work was done while hosted as a guest of the Automation of Logic group in the Max Planck Institut für Informatik.
*** Supported by the German Federal Ministry of Education and Research (BMBF) in the framework of the Verisoft XT project under grant 01 IS 07 008.


There is a well established infrastructure that supports research, development, and deployment of first-order Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library. This infrastructure has been central to the progress that has been made in the development of high performance first-order ATP systems. Until recently there has been no corresponding support in higher-order logic. In 2008, work commenced on extending the TPTP to include problems in higher-order logic, and developing the corresponding infrastructure and resources. These efforts aim to have an analogous impact on the development of higher-order ATP systems. This is a description of the practical progress that has been made towards this goal.

The Higher-order TPTP

The Typed Higher-order Form (THF) Language

The TPTP language is a human-readable, easily machine-parsable, flexible and extensible language, suitable for writing both ATP problems and solutions. A particular feature of the TPTP language, which has been maintained in the THF part, is Prolog compatibility. The THF language for logical formulae is a syntactically conservative extension of the existing first-order TPTP language, adding constructs for higher-order logic. The THF language has been divided into three layers: THF0, THF, and THFX. The THF0 core language is based on Church's simple type theory, and provides the commonly used and accepted aspects of a higher-order logic language. The full THF language drops the differentiation between terms and types, thus providing a significantly richer type system, and adds the ability to reason about types. It additionally offers more term constructs, more type constructs, and more connectives. The extended THFX language adds constructs that are "syntactic sugar", but are usefully expressive.

Here is an example of a TPTP problem file in THF0. The constructs that are not part of the first-order TPTP language are:

Additional THF constructs, not shown in the example, are:

Collecting THF Problems, for the TPTP

TPTP v3.7.0 was released in March 2009. This was a beta release of the THF part of the TPTP, and contained higher-order problems in only the THF0 language. There were 1275 THF problem versions, stemming from 852 abstract problems, in ten domains:

1002 of the problems (78%) contain equality. 1166 of the problems (92%) are known or believed to be theorems, 26 (2%) are known or believed to be non-theorems, 4 (0%) are are known or believed to be unsatisfiable sets of formulae, 3 (0%) are are known or believed to be satisfiable sets of formulae, 68 (5%) are open, and the remaining 8 problems (0%) have unknown status. These problems can be downloaded as part of TPTP v3.7.0 from the TPTP web site, or browsed online. Many more problems are expected by the time TPTP v4.0.0 is released in August 2009.

TPTP Infrastructure for THF Problems

From a TPTP user perspective, the TPTP2X utility distributed with the TPTP will initially be most useful for manipulating THF problems. TPTP2X has been extended to read, manipulate, and output (pretty print) data in the full THF language. Additionally, format modules for outputting problems in the TPS, Twelf, OmDoc, and Isabelle formats have been implemented. The TPTP4X tool has also been extended to read, manipulate, and output data in the THF0 language, and will be extended to the full THF language in 2009.

The SystemOnTPTP interface for running ATP systems and tools on TPTP problems and solutions has been updated to deal with THF data, including use of the new higher-order formats output by TPTP2X.

Internally, an important resource is the Twelf-based type checking of THF problems, implemented by exporting a problem in Twelf format, and submitting the result to the Twelf tool. The BNF based parsers for the TPTP naturally parse the full THF language, and the lex/yacc files used to build these parsers are freely available.

Collecting Solutions to THF Problems, for the TSTP

The Thousands of Solutions from Theorem Provers (TSTP) solution library, the "flip side" of the TPTP, is a corpus of contemporary ATP systems' solutions to the TPTP problems. Three higher-order ATP systems, LEO-II 0.99a, TPS 3.0, and two automated versions of Isabelle 2008 (one - IsabelleP - trying to prove theorems, the other - IsabelleM - trying to find (counter-)models), have been run over the 1275 THF problems in TPTP v3.7.0, and their results added to the TSTP. The systems are described below. This table tabulates the numbers of problems solved. The results show that the GRA Ramsey number problems are very difficult - this was expected. For the remaining domains the problems pose interesting challenges for the ATP systems, are the differences between the systems lead to different problems being solved, including some that are solved uniquely by each of the systems.


Problems 50 93 61 221 5 749 37 59 1275
THM/UNS 50 25 51 221 5 746 25 47 1170
CSA/SAT 0 0 10 0 0 3 5 11 29

LEO-II 0.99a 34 0 48 181 3 401 19 42 725 127
IsabelleP 2008 0 0 0 197 5 361 1 30 594 74
TPS 3.0 10 0 40 150 3 285 9 35 532 6
Any 32 0 50 203 5 490 20 52 843 207
All 0 0 0 134 2 214 0 22 372
None 18 93 12 18 0 259 17 15 432

IsabelleM 2008 0 0 1 0 0 0 0 8 9

Higher-Order ATP for the TPTP

Research and development of computer-supported reasoning for higher-order logic has been in progress for as long as that for first-order logic. It has become clear that the computational issues in the higher-order setting are significantly harder than those in first-order. Thus, while there are many interactive proof assistants based on some form of higher-order logic, there are few automated systems for higher-order logic. The three (fully automatic) higher-order ATP systems that we know of are LEO-II, TPS, and IsabelleP/M. These are available for use in the SystemOnTPTP interface.


LEO-II is a resolution based higher-order ATP system. LEO-II is implemented in Objective Caml, and is freely available under a BSD like licence. LEO-II is designed to cooperate with specialist systems for fragments of higher-order logic. Currently, LEO-II is capable of cooperating with the first-order ATP systems E, SPASS, and Vampire. LEO-II directly parses THF0 input, communicates with the cooperating first-order ATP system uses TPTP standards, has been debugged using examples in the TPTP library, and will soon produce THF0 output.


TPS is a higher-order theorem proving system that has been developed under the supervision of Peter B. Andrews since the 1980s. Theorems can be proven either interactively or automatically. In TPS there are flags that can be set to affect the behavior of automated search. The automated TPS used for solving THF problems uses two different collections of flags, in modes called MS98-FO-MODE and BASIC-MS04-2-MODE. As the two modes have quite different capabilities, they are run in competition parallel as a simple way of obtaining greater coverage. It was this competition parallel version of TPS that produced the 532 proofs noted in the table above.

IsabelleP and IsabelleM

Isabelle is a proof assistant for higher-order logic, which is normally used interactively. A fully automatic version, called IsabelleP, has been implemented using strategy scheduling of the nine automatic tactics simp, blast, auto, metis, fast, fastsimp, best, force, and meson. While it was probably never intended to use Isabelle as a fully automatic system, this simple automation provides useful capability. The ability of Isabelle to find (counter-)models using the refute tactic has also been integrated into an automatic system, called IsabelleM.

Current Work

Users and developers of ATP for higher-order logic are encouraged to submit higher-order problems to the TPTP, and to enter systems into CASC-22. Questions, suggestions, and contributions should be sent to Geoff Sutcliffe.


RDP 2009, Fed. Conf. on Rewriting, Deduction, and Programming

The Federated conference on Rewriting, Deduction, and Programming will take place on June 28 to July 03, 2009, in Brasília, Brazil.

It consists of two main events:

There are a number of collocated events, namely:

Early registration closes on May 1.

See the conference web page for full details!

CICM, Conferences on Intelligent Computer Mathematics

This is a federated conference that will take place on July 6–12, 2009 in Ontario, Canada.

It consists of two conferences:

Additionally, there will be the following workshops:

See the conference web page for full details on all events.

TABLEAUX 2009, Automated Reasoning with Analytic Tableaux and Related Methods

The next International Conference on Automated Reasoning with Analytic Tableaux and Related Methods will take place in Oslo, Norway, July 6–10, 2009.

TABLEAUX 2009 will be collocated with FTP 2009.

There will be three smaller workshops on July 6:

Submission to all three workshops is still possible.

Two tutorials will be part of the Tableaux programme:

Registration will open soon, early registration will be possible until June 5.

For full details about this event, please refer to the conference web pages

CADE-22: The Intl. Conference on Automated Deduction

This year's International Conference on Automated Deductions will be hosted by McGill University, Montreal, Canada August 2–7, 2009.

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

The following subsidiary events will be part of CADE this year:

Submission to all workshops is still possible!

Registration will open around May 20. The deadline for early registration is June 30.

See here for full details on this conference.

TPHOLs, Theorem Proving in Higher-Order Logics

The 22th International Conference on Theorem Proving in Higher Order Logics, TPHOLs, will take place on August 17–20, 2009 in Munich, Germany.

TPHOLs is a series of international conferences that brings together researchers working in all areas of interactive theorem proving, higher-order logics, and related topics.

The following workshops will be collocated with TPHOLs:

See the conference web page for full details!

FroCoS'09, Frontiers of Combining Systems

This symposium well take place in Trento, Italy, on September 16–18th, 2009.

FroCoS wants to offer a common forum for research activities in the general area of combination, modularization and integration of systems (with emphasis on logic-based ones), and of their practical use. Topics of interest include (but are not limited to):

Proceedings will be published in the Springer LNAI series.

Abstract submission deadline: April 26th, 2009
Full paper submission deadline: May 3rd, 2009

See the conference web page for further details.

The Intl. Tbilisi Symposium on Language, Logic and Computation

This symposium will take place in Bakuriani, Georgia, September 21–25, 2009.

The program committee invites submissions of two page abstracts on all aspects of language, logic and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:

The submission deadline is May 1, 2009 ; notification is due June 15. Accepted submissions will appear in the conference proceedings. The proceedings of the Six and Seventh International Tbilisi Symposium have been published in the LNAI series with Springer.

See the conference web page for details.


FTP 2009, the Workshop on First-Order Theorem Proving

This years FTP workshop will take place in Oslo, Norway, July 6–7, 2009. FTP be collocated with the Tableaux conference.

The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including (but not restricted to):

The deadline for paper submissions is April 20.

Accepted submissions will be published as a technical report of the University of Oslo. They will also be available on the web. As for the previous editions of FTP, a journal special issue is planned after the workshop.

Check the workshop web page for further details.

VLL, Workshop on Visual Languages and Logic

This workshop will take place In Corvallis, Oregon, US, on September 20, 2009.

The purpose of the VLL workshop is to explore the current state of research at the intersection of logic and visual languages, examining notations or software in which a graphical structure provides the foundation for, or a visualisation of, a system of logic. Topics of interest include, but are not limited to:

The submission deadline is June 22, 2009.

See the event's web page for full details.

Special Issues

Special Issue of Studia Logica: The Contributions of Logic to the Foundations of Physics

The special issue specifically, though not exclusively, invites contributions on the following topics:


The full CfP, including submission instructions is available in PDF format here


System Announcement: the ProofWeb system

ProofWeb is a system for using proof assistants (also known as interactive theorem provers) through the web. It is taylored specifically to practising natural deduction in logic courses. The ProofWeb home page which is the entry point into the system, and which contains all relevant information about it can be found at:

ProofWeb can be used for free, even without registration. It can be used with just a web browser, without even installing a plug-in. ProofWeb was developed to be used with the logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan which is published by Cambridge University Press, but it also can be used in conjunction with other textbooks. ProofWeb both supports "Gentzen-style" natural deduction in which proofs are tree-like derivation, and "Fitch-style" natural deduction in which proofs are lists of lines that grouped using boxes or "flags". ProofWeb was developed for the Coq proof assistant, but has been extended to various other proof assistants. ProofWeb is already being used in several proof assistant courses and introductory logic courses.

ProofWeb has been used in prototypes for more ambitious systems, most notably in the MathWiki prototype for a Wikipedia-like system that is integrated with on-line proof assistants, and the PC-Extra calculator which can calculate numerical expressions to arbitrary precision and where the correctness of the answers is simultaneously being proved by Coq.

ProofWeb was developed in the Netherlands at the Radboud University Nijmegen and Free University Amsterdam with money from the SURF Foundation. The developer of the ProofWeb system is Cezary Kaliszyk from the Radboud University. Currently the other members of the ProofWeb team are Dan Synek, Femke van Raamsdonk, Freek Wiedijk, Herman Geuvers and James McKinna.

Book Announcement: Handbook of Practical Logic and Automated Reasoning

John Harrison

Cambridge University Press 2009, 702 pages

ISBN: 9780521899574

The sheer complexity of computer systems has meant that automated reasoning, i.e. the ability of computers to perform logical inference, has become a vital component of program construction and of programming language design. This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.

For more information, see the publisher's web page.

For code and resources, see here.