{"entities":{"Q679255":{"pageid":681104,"ns":120,"title":"Item:Q679255","lastrevid":63531822,"modified":"2026-04-11T13:48:07Z","type":"item","id":"Q679255","labels":{"en":{"language":"en","value":"An erratum for some errata to ATP problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1002307"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$F5012E0C-BB4E-41AD-BE66-4A35CCDE7173","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2873d7741e0ec99076e8b5fbbe62b960778ecbf5","datavalue":{"value":{"text":"An erratum for some errata to ATP problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q679255$EC529241-EB96-49B5-977B-22DAEBAEA670","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cb2f317f0e68854e6d57e2c4ea0efc3e4161f6ae","datavalue":{"value":"0868.68099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$D92711FA-FD62-4C54-A00A-E0E4BC7FD6F7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"20d3e897237d63a4411635b7f20f8aa75b457a05","datavalue":{"value":"10.1023/A:1005764705033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$DE47FBC8-3C44-4077-927E-EDFB473008AB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5f25aab4c6b00769b6480f5283f54feec0bb72d4","datavalue":{"value":{"entity-type":"item","numeric-id":679253,"id":"Q679253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$C59D69D7-848A-4E22-A52D-5A452A9189B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c6d707c999cc6d62a42a2f34c4e05c6ede74383","datavalue":{"value":{"entity-type":"item","numeric-id":679254,"id":"Q679254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$F9B01ACE-6979-4289-A686-B89051C119FE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$CA0C6F06-D1BC-4BD1-A665-03FCAC55AE0A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"238dffa3abfa32d2f3f435b98c739e32735e84ac","datavalue":{"value":{"time":"+1997-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q679255$4E7313E3-BD2D-499F-9B89-945C09896D86","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"699216c9e4d19189c62adfe7bb266cce00ab7d7a","datavalue":{"value":"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.","type":"string"},"datatype":"string"},"type":"statement","id":"Q679255$02244D92-C439-4310-83C4-467AC6C9B400","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$824D7AD4-53FC-4766-B55A-C82DBBF4C882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$FAA4CCAE-47F4-4941-BBD1-10264EAB8B98","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1ff6d5be43bb3e08c9786f0fee55bf964facacc8","datavalue":{"value":"1002307","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$86403E1C-C6B2-41DD-BA49-545E48B09EC2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c837bf70f5985c7ee8bfdb9850d9bcdfdc5d2ff3","datavalue":{"value":"natural first-order form","type":"string"},"datatype":"string"},"type":"statement","id":"Q679255$8A52B793-8D9F-4270-882C-C961FEF076CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f5449e48d6f7d97dc09df56e0401b308409bd10","datavalue":{"value":"negated conclusion clause normal form","type":"string"},"datatype":"string"},"type":"statement","id":"Q679255$48D92EAC-71CA-4A8B-B8D3-2FF26B2E8E77","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$4447261C-7B5A-44D3-B36B-6AFEE6C8574A","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679255$6DA19317-4EFF-4D70-AD04-7FDD2A7B739E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cc564ad01810c4182c4b4d7324d6a41ab00944fc","datavalue":{"value":"https://doi.org/10.1023/a:1005764705033","type":"string"},"datatype":"url"},"type":"statement","id":"Q679255$55D5ECE0-4CD0-42ED-95E1-D14489C31677","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"38f2146b0e0908a81afcbb1785a76aa43947e98d","datavalue":{"value":"W1539833609","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679255$D576BB70-9B7A-4C74-8CE3-4B0A24A3CDC6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"260eefc72aa311745d2132d6e821d1459cd8f936","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fecd268ecc79d0649fbde069dac237f752ccaf48","datavalue":{"value":{"amount":"+0.7219143509864807","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q679255$8DC16682-1445-4C2C-B9F6-73D70DBF4B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af82521c3a0087569af5fb986fd5dc32a05cff95","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a7a914924bf92cb031e89dd139d0314e38dd915","datavalue":{"value":{"amount":"+0.7172040939331055","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q679255$E65703DA-EA61-45A1-8487-4F003200AC41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f103237e1b4889a22b078c6687a2ac0c70875b","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f524d6931fe885457088af63d5ab099f92066347","datavalue":{"value":{"amount":"+0.7165670394897461","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q679255$8CAA5AA7-A698-4855-AA2F-9776D84BD1FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2c14ed20a48c3aab929077d06fb2b3dc501071a","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a168c2767d74b238d769018eb2011198cff2f04","datavalue":{"value":{"amount":"+0.7043330669403076","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q679255$2A3AB954-2D92-4598-8968-0E2E37AFCE3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5b91b983fa2c75285aa70d29c690c153aac91f0","datavalue":{"value":{"entity-type":"item","numeric-id":3142015,"id":"Q3142015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f148e098cdefe2897cd24a2636627d8182eb120","datavalue":{"value":{"amount":"+0.6737045049667358","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q679255$CACAC7CE-2702-4906-91E7-76DC16D76D19","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An erratum for some errata to ATP problems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_erratum_for_some_errata_to_ATP_problems"}}}}}