An Erratum for Some Errata to Automated Theorem Proving Problems

• Author(s) / Creator(s)

  • Pelletier, Francis J.
  • Sutcliffe, Geoff

• Introduction: In 1986 Pelletier published an annotated list of logic problems, intended as an aid for students, developers, and researchers to test their automated theorem proving (ATP) systems. The 75 problems in the list are subdivided into propositional logic (Problems 1-17), monadic-predicate logic (Problems 18-34), full predicate logic without identity and functions (Problems 35-47), full predicate logic with identity but without functions (Problems 48-55), full predicate logic with identity and arbitrary functions (Problems 56-70), and problems to use in studying computational complexity of ATP systems (Problems 71-75). The problems were chosen partially for their historical interest and partially for their abilities to test different aspects of ATP systems. The problems were also assigned an intuitive \"degree of difficulty\", relativized to the type of problem. All the problems are presented in a \"natural form\" (which is here also called the \"first-order form\" or FOF), and most of them are also given in an equivalent negated conclusion clause normal form (CNF). The CNF versions of the problems are all in the TPTP Problem Library, and are thus conveniently available to ATP system developers who use the CNF form.

• Date created

  1995

• Subjects / Keywords

  • Logic
  • ATP systems

• Type of Item

  Article (Published)

• DOI

  https://doi.org/10.7939/R3NZ8146J

• License

  © 1995 Francis J. Pelletier et al. This version of this article is open access and can be downloaded and shared. The original author(s) and source must be cited.