An erratum for some errata to ATP problems
In 1986 \textit{F. J. Pelletier} published [ibid. 2, 191-216 (1986; Zbl 0642.68147)] an annotated list of 75 logic problems for testing ATP systems. The problems are presented in a natural first-order form (FOF), and most of them are also given in an equivalent negated conclusion clause normal form (CNF). The CNF versions are available in the TPTP Problem Library [\textit{G. Sutcliffe}, \textit{C. Suttner} and \textit{T. Yemenis}, ``The TPTP problem library, in: A. Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction, Sci., Lect. Notes Artif. Intell. 814, 252-266 (1994)]. Shortly after the publication of Pelletier's paper [loc. cit.], some errata were published [ibid. 4, 235-236 (1988; Zbl 0642.68148)]. In particular, Problem 62 was `corrected'. Recently, howeve, it has been discovered that both the CNF and FOF versions of Problem 62 in the errata are incorrect (although the FOF, unlike the CNF, is still a theorem). The correct version of Problem 62 is given.
- The TPTP problem library. CNF release v1. 2. 1
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The TPTP problem library
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- scientific article; zbMATH DE number 440107
This page was built for publication: An erratum for some errata to ATP problems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q679255)
