AARNEWS - December 2004

ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 65, December 2004

From the AAR President
Call for Papers

  • TIME 2005
  • SPIN 2005
  • FroCoS 2005
  • PPDP 2005
  • LICS 2005
  • KI 2005
  • IWIL-2005
  • ESSLL1'05 Student Session

  • CADE News: CADE-20
    CADE News: Announcement of CADE Elections
    TPTP Problem Library, Release v3.0.0

    From the AAR President, Larry Wos...

    I am pleased to include in this issue a brief article by Lis Jump. Lis and I worked together briefly; I taught her a bit about automated reasoning, and she proceeded to "beat the teacher" -- by finding a far shorter proof than I had found of a particular problem in group theory. I encourage all of you now to try to "beat the student" or, better, to send us equally challenging problems. I firmly believe that such experimentation is the way to ever-more-powerful automated reasoning programs. (And then, you may announce your successes at one or more of the many conferences and workshops announced in this issue of the AAR Newsletter.

    Using Otter to Obtain a Shorter Proof


    Lisabeth Jump

    I have been studying automated reasoning with Dr. Larry Wos. As part of my studies, he suggested I revisit a problem from group theory that he had proven a few years ago. Wos used Otter to prove that Dr. Bill McCune's single axiom for groups of exponent 5 was indeed a single axiom. In short, the problem required that I prove

      f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = y
    
    implies
                f(f(a,b),c) = f(a,f(b,c))
      f(a,f(a,f(a,f(a,a)))) = e
                     f(e,a) = a
    

    with a single input file. Wos had originally obtained a 62-step forward proof of the above with no demodulation. I set out to use Otter to do something similar and in the process to learn more about automated reasoning.

    Finding a forward proof of the theorem without using demodulation was nontrivial. Originally, I tried using Knuth-Bendix to find a proof and then eliminate demodulators individually, but had no success, so I started anew with a different tactic. First, I obtained a forward demodulation-free proof of the left identity. I added all of the steps of the proof to the hints list and moved left identity from the passive list to the set of support to create a different search space. Using this new search space, I achieved a forward proof of exponent five. I then eliminated the demodulators one at a time until the proof was demodulation free. I moved the steps of the new proof to the hints list and returned left identity from sos back to passive to obtain a forward proof of both left identity and exponent five with no demodulation. Finally, I replaced the current hints list with the hints generated from that proof and placed both left identity and exponent five in the set of support to try and obtain a proof of associativity. I proved associativity similarly, though it required a little more finesse. After this stage my proof was about 75 steps. This technique led me to a considerably different proof from the one obtained by Wos.

    I then took my proof and attempted to shorten it. First, I took each step of the proof, individually, and demodulated it to junk so that it would not be available in the new proof. I considered all of the results and chose a few of the shortest, repeating the process until I was no longer obtaining shorter proofs. Then I had three different proofs, all about 68 steps long. Next, I experimented with various parameters for these proofs. I had the most success when I changed the backward subsumption hint weight from one to ten and set the order equations flag. This brought me a proof of 63 steps.

    I took the 63-step proof and alternated between demodulating proof steps to junk and experimenting with various parameters. Using this method, I obtained a proof of 54 steps. Finally, at Wos's suggestion I placed the one axiom in the hot list, set heat to one, and repeated everything above. With this, I achieved a 51-step proof.

    The final proof that I obtained had only sixteen steps in common with Wos's original 62-step proof. These include the three axioms required for the proof and the hypothesis.

    Interested readers may examine the input file and proof , respectively.

    Call for Papers

    TIME 2005

    The 12th International Symposium on Temporal Representation and Reasoning will take place in Burlington, Vermont, June 23-25, 2005. Of interest is research on time-related problems within areas such as artificial intelligence, databases, and logic and computer-aided verification. Special emphasis is on new directions in time research. All submissions must be done electronically through the symposium Web page. The submission deadline is January 22, 2005.

    SPIN 2005

    The 12th international SPIN Workshop on Model Checking of Software will be held in San Francisco on August 22-24, 2005. SPIN 2005 solicits previously unpublished, currently unsubmitted, original contributions addressing theoretical, experimental and applied problems in model checking of software artifacts. Although authors are encouraged to compare their work with existing model checkers such as SPIN, the scope of the workshop is not limited to topics directly related to the SPIN system. Accepted contributions will be included in the workshop proceedings which will be published by Springer Verlag in the Lecture Notes in Computer Science series. The submission deadline: April 1 (abstracts) and April 8, 2005 (papers). For further information, see the Web site.

    FroCoS 2005

    The 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005) will be held at Vienna, Austria, September 19-21, 2005. The general theme of FroCoS is the development of techniques and methods for the combination, modularization and integration of systems (with emphasis on logic-based ones), and of their practical use.

    Topics of interest include the following:

    Submission categories include full papers, for work on foundations, applications, implementation techniques, and problem sets (up to 15 pages), as well as system descriptions (up to 8 pages), for describing publicly available systems. The submission deadline is May 2, 2005, for titles and abstracts, and May 9, 2005, for papers. For further information see the Web site.

    PPDP 2005

    The seventh ACM-SIGPLAN international symposium on Principles and Practice of Declarative Programming (PPDP 2005) will be held July 11-13, 2005, in Lisboa, Portugal.

    PPDP 2005 aims to provide a forum that brings together those in the declarative programming communities, including those working in the logic, constraint and functional programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for specifying, performing, and analyzing computations, and to stimulate cross-fertilization by including work from one community that could be of particular interest and relevance to the others.

    Topics include logic, constraint, and functional programming; applications of declarative programming; methodologies for program design and development; declarative aspects of object-oriented programming; concurrent extensions to declarative languages; declarative mobile computing; integration of paradigms; proof theoretic and semantic foundations; type and module systems; program analysis and verification; program transformation; abstract machines and compilation; and programming environments.

    The submission deadline is Feb. 13, 2005. Consult the Web for further details:

    LICS 2005

    The twentieth annual IEEE symposium on Logic in Computer Science (LICS 2005) will take place June 26-29, 2005, in Chicago, Illinois.

    The LICS symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic broadly construed. Submissions are invited on topics that fit under that rubric, including automated deduction, categorical models and logics, constraint programming, formal aspects of program analysis, formal methods, lambda and combinatory calculi, logics in artificial intelligence, modal and temporal logics, model checking, reasoning about security, rewriting, type systems and type theory, and verification. Also welcome are submissions in emergent areas, such as bioinformatics and quantum computation, if they have a substantial connection with logic.

    Authors are required to submit a paper title and a short abstract of about 100 words before submitting the extended abstract of the paper. All submissions must be electronic. Titles and short abstracts are due Jan. 5, 2005; extended abstracts are due Jan. 10, 2005. Authors will be notified of acceptance by March 18, 2005. Detailed information about electronic paper submission will be posted at the LICS Web site.

    Short Presentations: LICS 2005 will have a session of short (5-10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages long), should be entered at the LICS 2005 submission site March 19-25, 2005. Authors will be notified of acceptance or rejection by April 1, 2005.

    Kleene Award for Best Student Paper: An award in honor of the late S. C. Kleene will be given for the best student paper, as judged by the program committee. Details concerning eligibility criteria and procedure for consideration for this award will be posted at the LICS website. The program committee may decline to make the award or may split it among several papers.

    KI 2005

    The 28th German conference on AI will take place in Koblenz, Germany, on September 11-14, 2005. This conference traditionally brings together academic and industrial researchers from all areas of AI. Researchers are invited to submit proposals for technical papers and workshops/tutorials. Workshop/tutorial proposals must be submitted by February 18, 2005. The deadline for submission of technical papers is April 15, 2005.

    For detailed information see the Web site on workshops and on tutorials.

    IWIL-2005

    The fifth international workshop on the Implementation of Logics will be held in March 2005 in conjunction with the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Mondevideo, Uruguay.

    Contributions are invited that describe implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include the following:

    Of especial interest are contributions that help the community understand how to build useful and powerful reasoning systems.

    Researchers interested in participating are invited to send a short abstract (4-8 pages) to schulz@eprover.org by Jan. 14, 2005. Submissions should be in standard-conforming Postscript, PDF, or plain ASCII. Final versions will likely be required to be in Postscript or PDF and will be included in the proceedings. If possible, please use (PDF)LaTeX and the standard article class. Authors will be notified Feb. 11, 2005.

    For information, see the Web page.

    ESSLLI'05 Student Session

    The 17th European Summer School in Logic, Language and Information (ESSLLI'05) will be held August 8-19, 2005, in Edinburgh. Included will be a Student Session (StuS), and students (undergraduates as well as graduates) are invited to submit papers for oral and poster presentation from the areas of logic, language, and computation. Student authors are invited to submit a full paper, not to exceed 7 pages (exclusive of references). Papers are to be submitted with clear indications of the selected modality of presentation: oral or poster. The submissions will be reviewed by the student session program committee and selected reviewers. The preferred formats of submissions are PostScript, PDF, or plain text, although other formats will also be accepted. The paper and a separate identification page must be sent electronically to gervain@sissa.it by Feb. 15, 2005.

    For more information and the technical details of the submission, see the Web page.

    CADE News: CADE-20

    The 20th international Conference on Automated Deduction will take place in Tallinn, Estonia, July 22-27, 2005.

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

    Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory.

    Methods of interest include saturation, resolution, tableaux, sequent calculi, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, natural deduction, proof planning, proof presentation, proof checking, and explanation.

    Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI.

    Authors are invited to submit electronically (in postscript or PDF) full papers for work on foundations, applications or implementation techniques (15 pages), as well as system descriptions (5 pages) for describing publicly available systems. For further information and submission instructions, see the CADE-20 Web page.

    Deadlines:

    E-submission of title and abstract: February 25, 2005 E-submission papers: March 4, 2005 Notification of acceptance: April 22, 2005 Final version due: May 20, 2005

    Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles Dowek (Ecole Polytechnique) and by Frank Wolter (U. Liverpool).

    CADE News: Results of the CADE Trustee Elections 2004

    Amy Felty
    (Secretary of AAR and CADE)
    E-mail: afelty@site.uottawa.ca

    An election was held from September 23 through October 13 to fill four positions on the board of trustees of CADE Inc. Maria Paola Bonacina, David Basin, Gilles Dowek, Juergen Giesl, Rajeev Goré, Hans de Nivelle, Geoff Sutcliffe, and Cesare Tinelli were nominated for these positions. (See AAR Newsletter No. 64, September 2004.)

    Ballots were sent by electronic mail to all members of AAR on September 23rd, for a total of 630 ballots (up from 587 in 2003, 566 in 2002, 548 in 2001, 445 in 2000 and 396 in 1999). Of these, 125 were returned with a vote, representing a participation level of 19.8% (the same percentage exactly as in 2003, but down from 26.3% in 2002, 22.5% in 2001, 24.5% in 2000, and 30% in 1999). The majority is 50% of the votes plus 1, hence 63.

    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. 7th pref. 8th pref. Total
    M. P. Bonacina 30 22 22 15 3 0 2 31 125
    D. Basin 22 19 9 13 5 5 3 49 125
    G. Dowek 7 14 14 11 1 5 8 65 125
    J. Giesl 10 10 11 10 7 9 3 65 125
    R. Goré 15 18 17 13 3 4 0 55 125
    H. de Nivelle 7 11 16 17 4 7 8 55 125
    G. Sutcliffe 21 15 14 13 5 0 4 53 125
    C. Tinelli 13 13 15 15 9 4 4 52 125

    No candidate reaches a majority right away. G. Dowek and H. de Nivelle have the same number of first preference votes, but Dowek is higher in the ranking because of receiving more second preference votes. The redistribution of the votes of H. de Nivelle yields the following new distribution:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    M. P. Bonacina 31 22 22 15 2 1 22 10 125
    D. Basin 23 19 13 10 6 5 26 23 125
    G. Dowek 7 15 17 7 4 9 34 32 125
    J. Giesl 11 12 12 7 12 5 30 36 125
    R. Goré 18 16 19 10 4 3 29 26 125
    G. Sutcliffe 21 22 13 10 2 4 29 24 125
    C. Tinelli 14 15 20 11 7 6 28 24 125

    Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    M. P. Bonacina 31 30 18 12 2 7 20 5 125
    D. Basin 24 21 15 7 8 12 24 14 125
    J. Giesl 13 10 13 13 9 13 34 20 125
    R. Goré 20 16 20 9 4 15 25 16 125
    G. Sutcliffe 23 22 15 8 3 18 24 12 125
    C. Tinelli 14 20 22 7 8 18 20 16 125

    Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    M. P. Bonacina 33 31 21 7 6 11 14 2 125
    D. Basin 27 21 16 8 11 11 23 8 125
    R. Goré 22 17 20 10 11 12 23 10 125
    G. Sutcliffe 25 23 13 10 15 13 19 7 125
    C. Tinelli 17 19 20 12 15 13 22 7 125

    Again, no candidate reaches a majority, and 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. 7th pref. 8th pref. Total
    M. P. Bonacina 38 38 14 6 7 12 10 0 125
    D. Basin 30 23 18 8 8 23 13 2 125
    R. Goré 24 22 19 12 7 21 18 2 125
    G. Sutcliffe 29 22 14 17 10 17 13 3 125

    Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    M. P. Bonacina 46 42 6 5 13 8 5 0 125
    D. Basin 35 28 14 6 15 19 7 1 125
    G. Sutcliffe 36 21 23 6 17 11 10 1 125

    Again, no candidate reaches a majority, and by redistributing the votes of D. Basin, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    M. P. Bonacina 64 30 0 12 14 2 3 0 125
    G. Sutcliffe 44 36 1 12 21 7 3 1 125

    M. P. Bonacina is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    D. Basin 30 18 10 10 4 4 35 14 125
    G. Dowek 11 17 16 3 5 8 45 20 125
    J. Giesl 13 11 12 12 9 3 50 15 125
    R. Goré 17 27 16 5 5 0 41 14 125
    H. de Nivelle 11 16 19 9 7 8 45 10 125
    G. Sutcliffe 29 11 17 11 0 4 36 17 125
    C. Tinelli 13 21 19 10 5 5 36 16 125

    None of the candidates has a majority to be elected, so the votes of H. de Nivelle need to be redistributed again:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    D. Basin 32 17 15 6 6 15 31 3 125
    G. Dowek 11 21 13 5 9 19 42 5 125
    J. Giesl 15 12 13 14 5 20 41 5 125
    R. Goré 21 24 17 4 4 21 28 6 125
    G. Sutcliffe 31 16 17 4 4 18 29 6 125
    C. Tinelli 14 29 15 8 6 18 30 5 125

    Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    D. Basin 35 20 10 10 6 24 18 2 125
    J. Giesl 17 10 21 10 11 25 29 2 125
    R. Goré 24 25 14 6 12 20 21 3 125
    G. Sutcliffe 33 18 17 3 14 18 19 3 125
    C. Tinelli 15 37 11 6 16 14 24 2 125

    Again, no candidate reaches a majority, and 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. 7th pref. 8th pref. Total
    D. Basin 38 23 13 3 20 19 8 1 125
    J. Giesl 20 15 22 8 20 25 15 0 125
    R. Goré 28 30 7 10 19 20 9 2 125
    G. Sutcliffe 37 21 10 12 16 17 10 2 125

    Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    D. Basin 45 23 9 6 22 15 5 0 125
    R. Goré 32 30 13 5 22 16 7 0 125
    G. Sutcliffe 40 21 19 6 18 14 7 0 125

    Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    D. Basin 57 20 1 14 25 4 4 0 125
    G. Sutcliffe 49 31 1 15 17 7 5 0 125

    Thus, D. Basin is elected to the board of trustees. (Since 57 votes does not suffice for the majority, the STV algorithm executes another round distributing the votes of G. Sutcliffe, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 18 16 11 6 8 24 35 7 125
    J. Giesl 16 12 16 10 6 27 32 6 125
    R. Goré 26 27 10 7 0 22 27 6 125
    H. de Nivelle 12 23 16 11 8 25 27 3 125
    G. Sutcliffe 32 16 17 3 4 25 20 8 125
    C. Tinelli 20 19 19 8 7 23 22 7 125

    Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 19 18 11 10 10 35 20 2 125
    J. Giesl 18 14 18 9 11 31 23 1 125
    R. Goré 30 24 12 4 9 29 15 2 125
    G. Sutcliffe 35 24 8 5 13 23 14 3 125
    C. Tinelli 22 26 16 7 12 25 16 1 125

    Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 24 18 12 11 15 32 12 1 125
    R. Goré 35 23 12 5 14 27 8 1 125
    G. Sutcliffe 38 23 11 9 16 17 10 1 125
    C. Tinelli 25 25 19 10 15 22 9 0 125

    Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    R. Goré 42 20 13 5 19 21 4 1 125
    G. Sutcliffe 43 26 12 5 19 16 3 1 125
    C. Tinelli 29 32 18 5 18 19 4 0 125

    Again, no candidate reaches a majority, and 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. 7th pref. 8th pref. Total
    R. Goré 50 25 0 14 26 6 4 0 125
    G. Sutcliffe 52 28 1 14 22 4 4 0 125

    Thus, G. Sutcliffe is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 22 16 11 7 18 32 16 3 125
    J. Giesl 20 15 13 12 15 34 14 2 125
    R. Goré 33 27 9 1 13 26 12 4 125
    H. de Nivelle 19 23 13 10 18 30 9 3 125
    C. Tinelli 29 19 16 9 12 24 13 3 125

    Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 24 18 12 12 21 32 4 2 125
    J. Giesl 23 18 15 10 24 26 8 1 125
    R. Goré 38 25 6 7 20 21 6 2 125
    C. Tinelli 35 23 12 9 18 20 7 1 125

    Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    G. Dowek 30 18 17 4 34 18 3 1 125
    R. Goré 45 23 7 4 28 14 3 1 125
    C. Tinelli 39 24 15 5 27 10 5 0 125

    Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. 7th pref. 8th pref. Total
    R. Goré 54 21 0 14 26 7 2 1 125
    C. Tinelli 48 30 1 13 25 5 3 0 125

    Thus, R. Goré is elected to the board of trustees.

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

    Franz Baader (President, CADE-19 Program Chair, elected 10/2003)
    David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)
    Peter Baumgartner (elected 10/2003)
    Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)
    Amy Felty (Secretary, appointed 5/2004)
    Rajeev Goré (elected 10/2004)
    Michael Kohlhase (elected 10/2000, reelected 10/2003)
    Neil Murray (Treasurer)
    Robert Nieuwenhuis (CADE-20 Program Chair)
    Geoff Sutcliffe (elected 10/2004)
    Andrei Voronkov (Vice President, CADE-18 Program Chair, elected 10/2002)
    Toby Walsh (elected 10/2002)

    On behalf of the AAR and CADE Inc., I thank Frank Pfenning for his service as trustee and CADE Inc. president during the past 6 years, Gilles Dowek and John Harrison for their service as trustees during the past three years, all candidates for running in the election, all the members who voted; and offer congratulations to David Basin, Maria Paola Bonacina, Rajeev Goré, and Geoff Sutcliffe on being elected, and to Franz Baader on being elected president of CADE Inc.



    The TPTP Problem Library, Release v3.0.0

    (This release introduces the new TPTP syntax)
    Geoff Sutcliffe
    Dept. of Computer Science, University of Miami, USA
    geoff@cs.miami.edu

    The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with

    The principal motivation for this project is to move the testing and evaluation of ATP systems from the previously ad hoc situation onto a firm footing. This became necessary, as results being published do not always accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.

    TPTP v3.0.0 is now available on the Web. The TPTP-v3.0.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online.

    The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user and be kept informed of such developments, please email Geoff Sutcliffe.

    What's New in TPTP v3.0.0

    Changes from v2.7.0 to v3.0.0 for FOF problems

    Changes from v2.7.0 to v3.0.0 for CNF problems

    The library has been translated to the new TPTP syntax (aka the TSTP syntax).

    Equality is now assumed to be built in, and all equality axioms have been removed from all problems.

    Problem status values have been updated to the SZS problem status ontology:

    tptp1T has been updated to understand the new status values.

    No numbers appear in any problems--numbers are now reserved for future built-in treatment.

    The tptp2X utility has been extended and improved:


    Gail W. Pieper
    pieper@mcs.anl.gov
    December 2004