{"entities":{"Q4302847":{"pageid":6332448,"ns":120,"title":"Item:Q4302847","lastrevid":47265091,"modified":"2026-01-01T04:23:15Z","type":"item","id":"Q4302847","labels":{"en":{"language":"en","value":"Proving refutational completeness of theorem-proving strategies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 622327"}},"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":"Q4302847$E3EE4854-AF26-49DE-8C26-3EEE4334A785","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"add4dcf97bf2654039a3ad883e72928d454a92f5","datavalue":{"value":{"text":"Proving refutational completeness of theorem-proving strategies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4302847$467A13D7-9B0D-464D-B3B9-C6F6060005B7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"19e0303b905e6e677503e0c18d756749bb0b58c9","datavalue":{"value":"0799.68170","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$1967B15B-BE11-462B-AA18-609671D645A8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fa307dd17dada9fcae41684620361177e5dda5cb","datavalue":{"value":"10.1145/116825.116833","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$DB03164C-DF37-480F-9154-81A64CE36802","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5584b61080269b096f785173ffd49061cb7d63a9","datavalue":{"value":{"entity-type":"item","numeric-id":673133,"id":"Q673133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4302847$0E9846FC-AC07-4160-8289-AB3DD2490C54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d5450522126073beebe5b41bdc84b794c874c239","datavalue":{"value":{"entity-type":"item","numeric-id":437030,"id":"Q437030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4302847$1BAC8D90-229E-4043-9681-E48773D69D10","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f12bfc80fe4a431c556e028f5134a217234a7cc4","datavalue":{"value":{"entity-type":"item","numeric-id":63915,"id":"Q63915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4302847$249530B2-3F42-4243-A858-7E5A21FB9D44","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"aa19c9ba2bfb06d6b3228b43c9df9a36396a6316","datavalue":{"value":{"time":"+1994-08-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4302847$47BBDDC2-E286-493E-97F3-36C44B1855C5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$E1EF8C42-EDE0-4F0D-8734-CB0A44EACB29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$6DFD2E49-D60C-4287-8B66-F67E81F8FBB3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d28f86476850686229c505d9033fc47d20157b05","datavalue":{"value":"622327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$DBBB0B39-5786-447F-BE4E-E3E078EDE5C9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e1e6d4fc5112c631155052059c49a5ce5f42219","datavalue":{"value":"refutational theorem proving strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$36B35980-0AFD-4969-8C47-A2810E32824A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$11C8AC56-C557-4F58-B738-EBEDC191EED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f6a538f3561855eb60a330c94c2511b739e6e85","datavalue":{"value":"complete simplification orderings","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$4DA803DC-C5DF-4F57-8BC5-96EA1DC63F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$F45768AB-008F-47D4-ABAF-F99D2F9B1257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9f81fd79d9a404edbf19c987163b4693c5a6aa6","datavalue":{"value":"first-order logic with equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$E3E7DD27-C6B3-4EF6-899C-01E6ADC153CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b9360e246d1b227bf21c3be79e1089d80799523","datavalue":{"value":"functional reflexive axioms","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$76CF4E20-856A-4DF4-83D5-05784C209AA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f84bfa4d35417b90f2a3d3973763cb89a42b0a1","datavalue":{"value":"paramodulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$2F9AEA00-03EB-4CDC-AC2F-42044AE2A200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a733487313b5bc00626d9d92c91ea747b21c76f1","datavalue":{"value":"transfinite ordinals","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$61A9A37A-0EA7-49B3-ADC6-2D12F9226307","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eef7f586def24f3cdd9e8587f1cc13ec8cce693f","datavalue":{"value":"transfinite semantic trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$F97F2649-EE9A-42C2-A47A-A6E821315C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"56e0244404b4916c64679957351ef84322dac7ae","datavalue":{"value":"Wos-Robinson conjecture","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$81120380-6AA9-4DFF-9292-D1C4D0A6883F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"62ed1b2ba167230a9136fae7fa7f544041194248","datavalue":{"value":"Horn logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4302847$891C3F3E-EB07-44C8-B1DD-56F9A3BAB98A","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":"Q4302847$C1C6B338-4B99-48B4-B734-90AEAFCA575A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f30a200463ec73abba2dde65ce05183c139bf39","datavalue":{"value":"https://doi.org/10.1145/116825.116833","type":"string"},"datatype":"url"},"type":"statement","id":"Q4302847$82D7E166-9095-4A6F-B9E4-AD7882EDFBC5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"68c2c1e6712819324b8e2f4b1427c5aa375d5516","datavalue":{"value":"W2043314428","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4302847$DBD26818-44D3-4BE1-ADF5-B4B435F342A1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b15dd97b7846e68dab05b7f34aece11a43c5184c","datavalue":{"value":{"entity-type":"item","numeric-id":3786024,"id":"Q3786024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34f31501bd7f56f85d52a01326e5818200ca042c","datavalue":{"value":{"amount":"+0.9108423590660096","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":"Q4302847$14606445-A4AA-444C-A386-44136BC57547","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6da6700ed68850154ad19b69355723f73cba2748","datavalue":{"value":{"entity-type":"item","numeric-id":4647548,"id":"Q4647548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dbbfd0e5ad8fabf52fcac61572124db676ca2b4","datavalue":{"value":{"amount":"+0.8563957214355469","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":"Q4302847$B0159419-4C92-4C6C-8B31-4AD316038EB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663b4e5a63cb4379d9ebb8567a8fb5f4ba79e6ca","datavalue":{"value":{"entity-type":"item","numeric-id":757094,"id":"Q757094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59df3ea3ac167a488ec71264d0457468c658f119","datavalue":{"value":{"amount":"+0.8006367087364197","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":"Q4302847$7BC57A08-B8E4-4F23-BF89-93808D054DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edb9bc103ac6abca6432b206f30fd565c83d1948","datavalue":{"value":{"entity-type":"item","numeric-id":1209615,"id":"Q1209615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71081466885f1c6cee53e7e37806cfeccb8bcbaf","datavalue":{"value":{"amount":"+0.7771309614181519","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":"Q4302847$2E936B0A-C2C0-484A-92F1-170C2B8EE5C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47f6f8904700394da62e38c9b25fe7a94bd3f140","datavalue":{"value":{"entity-type":"item","numeric-id":1328182,"id":"Q1328182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71081466885f1c6cee53e7e37806cfeccb8bcbaf","datavalue":{"value":{"amount":"+0.7771309614181519","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":"Q4302847$BF2BE1D6-D353-438C-AD3F-96E080F3A52F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4302847","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4302847"}}}}}