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))))). % BCICandidate 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))). % BCICandidate 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 CADE22 conference, which focuses on logics and proofs.
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 exofficio trustee (as IJCAR 2008 program cochair), 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.
The newly formed board of trustees held an election of the CADE vicepresident, as the term of Reiner Hähnle as vicepresident was expiring. Reiner was renominated, 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 reelected.
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) tcs.inf.tudresden.de) with copies to Wolfgang Ahrendt (ahrendt (at) chalmers.se).
Nominations (including self nominations) are invited for the next EditorinChief 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 wellestablished 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
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.
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.
There is a well established infrastructure that supports research, development, and deployment of firstorder 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 firstorder ATP systems. Until recently there has been no corresponding support in higherorder logic. In 2008, work commenced on extending the TPTP to include problems in higherorder logic, and developing the corresponding infrastructure and resources. These efforts aim to have an analogous impact on the development of higherorder ATP systems. This is a description of the practical progress that has been made towards this goal.
The TPTP language is a humanreadable, easily machineparsable, 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 firstorder TPTP language, adding constructs for higherorder 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 higherorder 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 firstorder TPTP language are:
Additional THF constructs, not shown in the example, are:
TPTP v3.7.0 was released in March 2009. This was a beta release of the THF part of the TPTP, and contained higherorder 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 nontheorems, 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.
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 higherorder formats output by TPTP2X.
Internally, an important resource is the Twelfbased 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.
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 higherorder ATP systems, LEOII 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.
 
ALG  GRA  LCL  NUM  PUZ  SE?  SWV  SY?  Total  Unique  

 
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  
 
LEOII 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  

Research and development of computersupported reasoning for higherorder logic has been in progress for as long as that for firstorder logic. It has become clear that the computational issues in the higherorder setting are significantly harder than those in firstorder. Thus, while there are many interactive proof assistants based on some form of higherorder logic, there are few automated systems for higherorder logic. The three (fully automatic) higherorder ATP systems that we know of are LEOII, TPS, and IsabelleP/M. These are available for use in the SystemOnTPTP interface.
LEOII is a resolution based higherorder ATP system. LEOII is implemented in Objective Caml, and is freely available under a BSD like licence. LEOII is designed to cooperate with specialist systems for fragments of higherorder logic. Currently, LEOII is capable of cooperating with the firstorder ATP systems E, SPASS, and Vampire. LEOII directly parses THF0 input, communicates with the cooperating firstorder ATP system uses TPTP standards, has been debugged using examples in the TPTP library, and will soon produce THF0 output.
TPS is a higherorder 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 MS98FOMODE and BASICMS042MODE. 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.
Isabelle is a proof assistant for higherorder 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.
Users and developers of ATP for higherorder logic are encouraged to submit higherorder problems to the TPTP, and to enter systems into CASC22. Questions, suggestions, and contributions should be sent to Geoff Sutcliffe.
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!
This is a federated conference that will take place on July 6–12, 2009 in Ontario, Canada.
It consists of two conferences:
For short papers on emerging trends, the abstract submission deadline is April 30, and the submission deadline May 7, 2009.
Additionally, there will be the following workshops:
See the conference web page for full details on all events.
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
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.
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, higherorder logics, and related topics.
The following workshops will be collocated with TPHOLs:
See the conference web page for full details!
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 logicbased 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.
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.
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 firstorder classical, manyvalued, 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.
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.
The special issue specifically, though not exclusively, invites contributions on the following topics:
DEADLINE FOR SUBMISSION OF MANUSCRIPTS: May 31, 2009
The full CfP, including submission instructions is available in PDF format here
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 plugin. 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 "Gentzenstyle" natural deduction in which proofs are treelike derivation, and "Fitchstyle" 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 Wikipedialike system that is integrated with online proof assistants, and the PCExtra 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.
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 selfcontained and broadbased 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 onestop 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.