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
Call for Papers:

  • CSL'99
  • Sixth Workshop on Automated Reasoning
  • From the AAR President, Larry Wos...

    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.

    Can Your ATP System Solve These TPTP Problems?

    Geoff Sutcliffe

    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.


    [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.

    Typed Proof Problems Extracted from the Mizar Library

    Ingo Dahn, Universität Koblenz-Landau,
    Christoph Wernhard, Humboldt Universität Berlin,

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

    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

    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.

    New Book

    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.


    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
    Author Index
    Subject Index

    Abstracts of the Journal of Automated Reasoning

    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 News


    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

    Conference Calls


    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

    For further information, see the Web site.

    International Master's Program in Computational Logic

    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 Further information is on the Web.