An Erratum for Some Errata to Automated Theorem Proving Problems

Loading...
Thumbnail Image

Date

Citation for Previous Publication

Pelletier, F.J., & Sutcliffe, G. (1995). An Erratum for Some Errata to Automated Theorem Proving Problems. Newsletter of the Association for Automated Reasoning, 31, 8-14. https://mystelven.github.io/Association-Automated-Reasoning/Newsletters/031-1995-12.pdf

Link to Related Item

https://mystelven.github.io/Association-Automated-Reasoning/Newsletters/031-1995-12.pdf

Abstract

Description

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.

Item Type

http://purl.org/coar/resource_type/c_6501 http://purl.org/coar/version/c_970fb48d4fbd8a85

Alternative

License

Other License Text / Link

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

Subject/Keywords

Language

en

Location

Time Period

Source