NEWSLETTER

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:

Our first issue of the AAR Newsletter for 1999 offers numerous suggestions
for how to begin the new year:
browsing through a recent issue of the *Journal of Automated Reasoning*
or a new book on logic, preparing a submission for next year's conferences,
or--most satisfying to me--attacking problems in automated reasoning
or developing new reasoning procedures for typed proof problems.
Naturally, I, and AAR, would be very interested in hearing about your successes.

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:

ALG001-3 - Believed to be unsatisfiable

CIV002-1 - Believed to be unsatisfiable

COL069-1 - Believed to be satisfiable

COL073-1 - Believed to be satisfiable

FLD004-1 - Believed to be unsatisfiable

FLD013-1 - Believed to be unsatisfiable

FLD013-2 - Believed to be unsatisfiable

FLD025-1 - Believed to be unsatisfiable

FLD025-2 - Believed to be unsatisfiable

FLD060-2 - Believed to be unsatisfiable

FLD061-1 - Believed to be unsatisfiable

FLD061-2 - Believed to be unsatisfiable

FLD061-3 - Believed to be unsatisfiable

GEO001-4 - Believed to be unsatisfiable

GEO012-3 - Believed to be unsatisfiable

GRP025-3 - Believed to be unsatisfiable

GRP026-2 - Believed to be unsatisfiable

GRP026-3 - Believed to be unsatisfiable

GRP026-4 - Believed to be unsatisfiable

GRP027-1 - Believed to be unsatisfiable

GRP027-2 - Believed to be unsatisfiable

GRP081-1 - Believed to be satisfiable

GRP164-1 - Believed to be unsatisfiable

GRP164-2 - Believed to be unsatisfiable

GRP187-1 - Believed to be unsatisfiable

MSC008-1.010 - Believed to be satisfiable

NUM046-1 - Believed to be unsatisfiable

NUM061-1 - Believed to be unsatisfiable

NUM065-1 - Believed to be unsatisfiable

NUM136-1 - Believed to be unsatisfiable

NUM141-1 - Believed to be unsatisfiable

NUM142-1 - Believed to be unsatisfiable

NUM149-1 - Believed to be unsatisfiable

NUM159-1 - Believed to be unsatisfiable

NUM201-1 - Believed to be unsatisfiable

NUM232-1 - Believed to be unsatisfiable

NUM235-1 - Believed to be unsatisfiable

NUM263-2 - Believed to be unsatisfiable

PUZ015-1 - Believed to be satisfiable

PUZ034-1.003 - Believed to be satisfiable

RNG001-2 - Believed to be unsatisfiable

RNG010-1 - Believed to be unsatisfiable

ROB001-1 - Believed to be unsatisfiable

ROB025-1 - Believed to be unsatisfiable

SET186-6 - Believed to be unsatisfiable

SET226-6 - Believed to be satisfiable

SET227-6 - Believed to be satisfiable

SET228-6 - Believed to be satisfiable

SET229-6 - Believed to be satisfiable

SET243-6 - Believed to be unsatisfiable

SET559-6 - Believed to be unsatisfiable

SET561-6 - Believed to be unsatisfiable

SET562-6 - Believed to be unsatisfiable

SET564-6 - Believed to be unsatisfiable

SET565-6 - Believed to be unsatisfiable

SET566-6 - Believed to be unsatisfiable

SYN067-2 - Believed to be unsatisfiable

SYN314-1.002:001 - Believed to be unsatisfiable

SYN421+1 - Believed to be satisfiable

SYN424+1 - Believed to be satisfiable

SYN427+1 - Believed to be satisfiable

SYN429-1 - Believed to be satisfiable

SYN437+1 - Believed to be satisfiable

SYN437-1 - Believed to be satisfiable

SYN439+1 - Believed to be a theorem

SYN439-1 - Believed to be unsatisfiable

SYN440+1 - Believed to be a theorem

SYN440-1 - Believed to be unsatisfiable

SYN447+1 - Believed to be a theorem

SYN447-1 - Believed to be unsatisfiable

SYN453+1 - Believed to be satisfiable

SYN457+1 - Believed to be a theorem

SYN457-1 - Believed to be unsatisfiable

SYN460+1 - Believed to be a theorem

SYN460-1 - Believed to be unsatisfiable

SYN464+1 - Believed to be satisfiable

SYN464-1 - Believed to be satisfiable

SYN466-1 - Believed to be unsatisfiable

SYN519+1 - Believed to be satisfiable

SYN520-1 - Believed to be satisfiable

TOP014-1 - Believed to be satisfiable

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.

Most realistic proof problems are formulated in a typed language. Nevertheless, automated theorem provers pay relatively little attention to the efficient use of type information.

In order to support appropriate experiments with modifications of existing theorem provers, we have extracted a set of proof problems from the Mizar Mathematical Library (www.mizar.org). These problems use several type constructors, some of them with parameters. In order to make the proof problems accessible for existing theorem provers, type information has been encoded in the most naive way by relativizations.

This approach has the advantages that

- the problems can be handled by any prover that uses untyped quantified first-order formulas, and
- type information can be easily recognized in the formulas.

By the first of these points, the problems can be directly given as input to existing provers. For example, Otter was able to solve 25 out of the 47 problems in auto mode. However, the performance of automated provers on these problems cannot be considered as satisfactory yet. For example, problem 19 in this collection was proved interactively in the Mizar library with two interactions. But a solution with the interactive ProofPad of the ILF system, delegating subproblems to the provers Spass and Setheo, required six interactions. For most problems, 3-4 interactions were necessary. This is mainly due to the fact that the Mizar verifier efficiently calculates types instead of searching for proofs of well-typedness.

The second point made above maybe helpful for the adaptation of theorem provers. We emphasize that it is not the main task to solve the problems in the form in which they are provided. Rather we should like to encourage the development of preprocessing or reasoning procedures appropriate to this kind of type systems.

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.

A new book *Effective Logic Computation*, by
K. Truemper, has been published by
John Wiley & Sons, Inc.
(1998,
ISBN 0-471-23886-4).
The book presents a new theory for
logic computation that supports the construction
of fast solution algorithms, with guaranteed performance,
for large classes of real-world problems.

The book is 476 pages and costs $79.95 in hardcover.

**Contents**

Introduction

Basic Concepts

Some Matroid Theory

System B, Linear Algebra, and Matroids

Special Matrix Classes

Characterizations of Hidden Near Negativity

Boolean Closed Matrices

Closed Subregion Decomposition

Monotone Sum

Closed Sum

Augmented Sum

Linear Sum

Analysis Algorithm

Central and Semicentral Classes

References

Author Index

Subject Index

Basic Concepts

Some Matroid Theory

System B, Linear Algebra, and Matroids

Special Matrix Classes

Characterizations of Hidden Near Negativity

Boolean Closed Matrices

Closed Subregion Decomposition

Monotone Sum

Closed Sum

Augmented Sum

Linear Sum

Analysis Algorithm

Central and Semicentral Classes

References

Author Index

Subject Index

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.

**CADE-16**

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 |

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

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.