No. 42 January 1999

Table of Contents

From the AAR President
Can Your ATP System Solve These TPTP Problems?
Typed Proof Problems Extracted from the Mizar Library
New Book: Effective Logic Computation
Abstracts of the Journal of Automated Reasoning
CADE News
Call for Papers:

From the AAR President, Larry Wos...

The TPTP (Thousands of Problems for Theorem Provers) Problem Library [SS98] has emerged as the standard problem set for testing first order automated theorem proving (ATP) systems. The TPTP may be obtained from the Web address.

Since the first release of the TPTP in 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation. Some researchers, who have tested their ATP systems over the entire TPTP, have made their results available. These results have been collected, and a summary can be seen on the Web.

This site also provides guidelines for submitting results to the collection. One of the uses of the results collection is to validate the status of the TPTP problems, one of unsatisfiable or satisfiable for CNF problems, and one of theorem or satisfiable for FOF (First Order Form) problems. There are some problems in the TPTP whose status is believed to be known, but for which the available result data does not validate their status (because the ATP systems failed to solve the problems within the resource limits allocated in their testing). The problems are as follows:

Researchers and research groups who have decent, running, fully automated ATP systems are challenged to test their ATP systems over the entire TPTP, and (it is hoped) provide results that will validate (or correct) the status of these problems.

Reference

[SS98] Sutcliffe, G., and Suttner, C. B. (1998), The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21(2) 177-203.

The problems can be downloaded in TPTP first-order format from our Web site. They contain all theorems of the Mizar article ``Relations Defined on Sets'' by Edmund Woronowicz (relset_1).

Each proof problem contains the theorem and the axioms that are explicitly referenced by the author of its Mizar proof. The proof problem is supplemented by additional axioms representing built-in facilities of the Mizar verifier. These include

• properties such as reflexivity, symmetry and commutativity that, once proved for an operator, can be tacitly used by the Mizar verifier,
• definitions of operators occurring in the theorem that can be unfolded by the Mizar verifier,
• axioms related to the type system, and
• redefinitions concerning operators occurring in the theorem.

Obviously a proof problem can therefore contain unnecessary axioms. Since the Mizar language and verifier have no specification, the choice of these auxiliary axioms had to be based on experiments and might be incomplete for some proof problems.

Nevertheless, the problem set represents several aspects that are important for many kinds of applications of automated theorem proving: It includes ``higher-level'' language features such as a type system, which are necessary for expressing mathematical knowledge at a larger scale. The axiomatization is at an abstraction level that is used in practice by mathematicians, in contrast to just basic set theory axioms. Potentially relevant axioms are preselected, as, for example, in a setting where automated provers are used to bridge gaps in interactive proving.

Related Papers

B. I. Dahn, Ch. Wernhard. First Order Proof Problems Extracted from an Article in the Mizar Mathematical Library. In Proc. of the International Workshop on First Order Theorem Proving, RISC-Linz Report Series, No. 97-50, Linz, 1997.

B. I. Dahn. Interpretation of a Mizar-like Logic in First Order Logic. To appear in Proc. of the Second International Workshop on First order Theorem Proving, 1998.

As most of you--I hope--are aware, your membership in the AAR entitles you to a substantial discount for a subscription to the Journal of Automated Reasoning. Here we give brief information about the past two issues of the journal. You may download the PostScript file.

As announced in an earlier AAR newsletter, CADE-16 will take place July 7-10, 1999, in Trento, Italy. Please note that the deadline for submissions has been changed to January 5, 1999. For further information, see the Web page.

CADE-Inc Trustees Election Results

The results of the ballot for election of CADE-Inc Trustees are as follows.

Eighty-four voters responded; and as a result of the votes cast, Claude Kirchner and Frank Pfenning were elected first and second respectively.

In detail, the STV algorithm produced the following three rounds of votes:

	Kirchner	Pfenning	Plaisted
Round 1	38	24	22

No candidate has a majority, so Plaisted temporarily removed and his votes redistributed.

	Kirchner	Pfenning
Round 2	50	33

Kirchner elected and his votes redistributed.

	Pfenning	Plaisted
Round 3	44	38

Pfenning elected.

Note: The reason why the votes do not always add up to 84 is that a few voters placed one candidate first and the other two last: redistribution of such a vote produces two new second preferences but no new first preference.

I hereby declare Claude Kirchner and Frank Pfenning duly elected to serve as Trustees for a period of three CADEs.

On behalf of the Trustees, I also extend thanks for their work on behalf of CADE to to Alan Bundy and Deepak Kapur whose terms as Trustees have now expired.

John Slaney
President, CADE-Inc

The composition of the Board of Trustees is now as follows:

Trustee	Term Begins	Term Ends
John Slaney (Pres)	CADE-13	1999 (CADE-16)
Bill McCune	CADE-14	2000 (CADE-17)
Uli Furbach	CADE-14	2000 (CADE-17)
Harald Ganzinger	PC for CADE-16	1999 (CADE-16)
Claude Kirchner	CADE-15	2001 (CADE-18)
Frank Pfenning	CADE-15	2001 (CADE-18)
Neil Murray (Sec/Treas)	CADE-11	indefinite

CSL'99

The annual conference of the European Association for Computer Science Logic (CSL'99) will take place September 20-25, 1999, in Madrid, Spain. The conference will cover a wide variety of areas including abstract datatypes, automated deduction, categorical and topological approaches, concurrency theory, constructive mathematics, database theory, domain theory, finite model theory, lambda and combinatory calculi, logical aspects of computational complexity, logical foundations of programming paradigms, linear logic, modal and temporal logics, model checking, program logics and semantics, program specification, transformation and verification, rewriting, and symbolic computation. The conference will include invited presentations by Jose Luis Balcazar, Javier Esparza, Martin Grohe, Peter D. Mosses, and Victor Vianu.

Authors are invited to submit papers (up to 15 pages) by March 19, 1999. Papers accepted by the Program Committee must be presented at the conference and will appear in a proceedings volume, to be published by Springer Verlag in the Lecture Notes in Computer Science series. For further information, see the Web site.

Sixth Workshop on Automated Reasoning

Abstract submissions and suggestions for panel sessions are invited for the Sixth Workshop on Automated Reasoning - Bridging the Gap between Theory and Practice, which will take place in Edinburgh, Scotland, on April 8-9, 1999.

The workshop aims to bring together researchers from all areas of automated reasoning in order to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines; among researchers from academia, industry and government; and between theoreticians and practitioners.

The format of the automated reasoning workshop this year will include invited speakers, panel discussions, contributed talks, and a poster session. Although there will be a number of "pre-arranged" items to be discussed during the workshop, it will cover the full breadth and diversity of automated reasoning, including topics such as logic and functional programming; equational reasoning; deductive databases; unification and constraint solving; the application of formal methods to specifying, deriving, transforming and verifying computer systems and in particular safety-critical systems; deductive and nondeductive reasoning, including abduction, induction, nonmonotonic reasoning, and analogical reasoning; commonsense reasoning; and the wide range of topics that fall under the heading of knowledge representation and reasoning.

Interested persons are invited to submit a two-page abstract by February 19, 1999, to
M.Kerber@cs.bham.ac.uk.

For further information, see the Web site.

The Dresden University of Technology is offering a two-year study program, in English, leading to a master of science in computational logic (together with a German ``Diplom in Informatik"). The program is sponsored by the European Network of Excellence in Computational Logic (COMPULOG Net) and other German institutions.

Courses focus on logic and constraint programming, artificial intelligence, type theory, model theory, proof theory, equational reasoning, databases, natural language processing, planning, and formal methods, among others.

The tuition fees are waived. At the end of the program a research master thesis must be discussed.

Prerequisites are a good knowledge of the basics of logic, and familiarity with mathematical reasoning. Knowledge of foundations of artificial intelligence and logic programming are desirable. Fluency in English is indispensable; German is not necessary, but there are facilities for studying it if desired. A bachelor's degree in computer science, or the equivalent, is required by the beginning of courses in October 1999.

The deadline for applications is June 30, 1999, but applications are processed as they come. To apply, just send an e-mail with your curriculum vitae to mailto:cl@pikas.inf.tu-dresden.de. Further information is on the Web.