An erratum for some errata to ATP problems
type: Item
instance of: scholarly article
title: An erratum for some errata to ATP problems
zbMATH Open document ID: 0868.68099
DOI: 10.1023/A:1005764705033
author: Francis Jeffry Pelletier
author: Geoff Sutcliffe
published in: Journal of Automated Reasoning
publication date: 1997-08-17T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1002307
zbMATH Keywords: natural first-order form
zbMATH Keywords: negated conclusion clause normal form
describes a project that uses: TPTP
MaRDI profile type: Publication
full work available at URL: a:1005764705033
OpenAlex ID: W1539833609
description: scientific article; zbMATH DE number 1002307