{"entities":{"Q3645586":{"pageid":5675492,"ns":120,"title":"Item:Q3645586","lastrevid":50826113,"modified":"2026-01-15T07:54:31Z","type":"item","id":"Q3645586","labels":{"en":{"language":"en","value":"Using \u00c6tnaNova to formally prove that the Davis-Putnam satisfiability test is correct"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5635094"}},"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":"Q3645586$9735D4A4-5D4B-484B-8FE5-CAA79A5D5082","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7313818e5b78509781887f09226b47ef73866863","datavalue":{"value":"1180.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$78A232A2-1DCF-4F45-B55C-E1E06743635B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fccb48273352f9d3a76d946d757d4f77a228b9e4","datavalue":{"value":{"entity-type":"item","numeric-id":400529,"id":"Q400529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3645586$D2F23D80-AAFE-49D0-ACC5-56A83EAD56CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9faadbd22dd8b1da3be6dbb593d6df9253bd99cd","datavalue":{"value":{"entity-type":"item","numeric-id":1248615,"id":"Q1248615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3645586$1AEA5165-1324-45AE-A832-B5839906E41F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d854bb3e97b3fd38c10eaa4e7365bd0951b145d2","datavalue":{"value":{"time":"+2009-11-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3645586$234C04C7-27A4-4C70-826F-632EC63AF14B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3b797121587bd2408da10f4c8ab5d98fdb225822","datavalue":{"value":"http://www.dmi.unict.it/ojs/index.php/lematematiche/article/view/49","type":"string"},"datatype":"url"},"type":"statement","id":"Q3645586$228B0112-8C5D-4865-8FE6-337E32540E2E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$2A43433F-97CB-4486-8B38-2102B30BC027","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d76b54ca3ec41228d05d0d48b5373554ccc0dcb3","datavalue":{"value":"03E30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$94BE5979-49A9-4B43-99E0-7647EF740ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$8AF373E5-4520-4B41-9364-CF1892CD72ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$98C7709E-D053-4DB4-BC7C-8DF23DFDCDE6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d5f744184284af4f8747dcf3aebb400dca1b44c1","datavalue":{"value":"5635094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3645586$01F5595C-139A-4210-B63F-DFA13756F725","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a614927b0caf638748bb51c0de92c1b49104311","datavalue":{"value":"proof checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$0C127470-6EDA-4E83-B9D3-FBC5FC46A125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef4d99f196f11514c6dd5672f20edcd9143f3477","datavalue":{"value":"program-correctness verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$6E2AC7D7-48EA-4BA3-A24A-EFE91110E86A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"79bc8909ce4636a0488fe1c98d1fee6f3e23a4b1","datavalue":{"value":"computable set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$8AE1BA8F-56E7-41A6-BFB4-D1BBE0C4C764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c60fc6c894016b42326cccd386f78134956ad54a","datavalue":{"value":"cumulative hierarchy","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$D354835C-DD5C-4AEC-9EA3-EA8886C75AE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c5c78d0a76c2813b02c697a91b8624cab72cc66","datavalue":{"value":"satisfiability decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$148310BF-485F-45B8-BE43-A7D7F022879E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da5f5f011fb5062545b0b3540f50d45b1f2d2243","datavalue":{"value":"proof modularization","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$836B3B54-2434-4F38-A74B-F2EECD153A3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f407eb74642f481c17e3bd91601648a74f4bcfdd","datavalue":{"value":"proof-verification system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3645586$06B643B7-7E78-4639-82C2-DEDE6A89B878","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":"Q3645586$E54CFEF3-18B4-4312-93E9-AFA46CE4AA66","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ad1ae46a13dbdff43b01ae1250f32f6cb7d67ad","datavalue":{"value":{"entity-type":"item","numeric-id":3562927,"id":"Q3562927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0ec2d5226b47fb02df8a7575bae624677483b66","datavalue":{"value":{"amount":"+0.7495766282081604","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":"Q3645586$CB7754E8-651F-4E90-AD0B-777B73554267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e366a6ae1ffcd391788169251187e485eed88162","datavalue":{"value":{"entity-type":"item","numeric-id":5687274,"id":"Q5687274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecae3af0eac32e773f801721629927b474caa937","datavalue":{"value":{"amount":"+0.7417612671852112","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":"Q3645586$591C48EE-DA34-40EE-8C46-4F49E68EFB4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"368b2fde13e02c4e6de0084f7da54d370829d06c","datavalue":{"value":{"entity-type":"item","numeric-id":1822244,"id":"Q1822244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecae3af0eac32e773f801721629927b474caa937","datavalue":{"value":{"amount":"+0.7417612671852112","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":"Q3645586$15034BF2-5E1E-41E1-B897-C63714E4C703","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"117a8384df9f2cfd5c63b60924d56a8724ff3cff","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fe037690d4e4d533478a046464258f1b635d768","datavalue":{"value":{"amount":"+0.736579418182373","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":"Q3645586$9763A05D-1C31-4F1F-B751-AA8C5D16B673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0a7d02cb164b0fef672b89a3290eea77a00927e","datavalue":{"value":{"entity-type":"item","numeric-id":2749864,"id":"Q2749864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0eb3036b1d0324e61f0a21fe551cf3c2b4c25092","datavalue":{"value":{"amount":"+0.7317632436752319","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":"Q3645586$AC28E108-296C-4DDA-A26D-B4384207647E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3645586","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3645586"}}}}}