{"entities":{"Q2784492":{"pageid":2795230,"ns":120,"title":"Item:Q2784492","lastrevid":47774122,"modified":"2026-01-02T16:03:11Z","type":"item","id":"Q2784492","labels":{"en":{"language":"en","value":"The efficiency of resolution and Davis-Putnam procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1732380"}},"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":"Q2784492$71926674-A947-4BBE-9529-1E20CF5F3BCA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e62fc6d62b325683ef54813e1999a9314d375fca","datavalue":{"value":"1004.03048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$2A2E03B3-9C65-44E9-A362-BAF7DDB8CA9C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5fd505f69de1bd6662271a7f3c19eb1614c64305","datavalue":{"value":"10.1137/S0097539700369156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$57EDCCC9-0743-4D8B-BBA0-FC6160C4897E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38b40ed6cb099fba5da493703b11839c0af89042","datavalue":{"value":{"entity-type":"item","numeric-id":202089,"id":"Q202089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2784492$F64E093A-E076-42C0-A8D7-40A7CC375F4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bdeac5e928e087a649bdeced20db2b34fab0678f","datavalue":{"value":{"entity-type":"item","numeric-id":1822913,"id":"Q1822913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2784492$00B47CC8-F019-48B9-91B9-CDEBCE49F110","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d7f03cf6abbdf2fe79063aacbf005af333537b97","datavalue":{"value":{"entity-type":"item","numeric-id":619905,"id":"Q619905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2784492$ABB1D215-8735-4C9E-B1C4-34D127D73BF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"93f09421b6aff8e8d7720ab7e9d35f10a9deb5a2","datavalue":{"value":{"entity-type":"item","numeric-id":1112076,"id":"Q1112076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2784492$B1361B8A-8C69-4D4A-A561-54E1951109C5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c2a1c45d0f0997786c62faf9f7fcd603424632e8","datavalue":{"value":{"entity-type":"item","numeric-id":84798,"id":"Q84798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2784492$3C4C4C6D-F3C7-4B54-BFCF-2BE3750407E6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"22e17fffa644ae9f618754e26357d6dbd53b7382","datavalue":{"value":{"time":"+2002-04-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2784492$BA1E8141-6C6D-4253-8568-CD70D3D900D3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$9F4E323D-94D2-441C-8D20-3DB9E9D21E9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$043B45DA-F3C8-4AE9-B6FE-39AAD6D07B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$F4F4D4D4-3C99-4313-8821-E66637868397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$856C296D-B3C9-4DA0-998B-B4F3CABD420B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$A9223652-B6BA-4B56-A4F4-C1F894A3101D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$FEA6F4CC-BD36-4489-AE97-6D256342957F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7ddaa80bf0a693a36c1113ff6b7ad576f729940","datavalue":{"value":"68W40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$DF1E52C7-FC46-4D94-8115-23A7E4E38B10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$524B86DF-3F34-438D-B3C9-941130F13A45","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d6e32276336c58b13c8a64993bdf3a3da6555369","datavalue":{"value":"1732380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$1C07ED31-D433-4A4D-8669-24369E10DE6B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$9795831A-23FA-4A46-8C48-647433F15FB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$5F967377-2FC0-4859-A6AF-08369CB763A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b2085f6ca6b5f22ff227aa538ed50fc77fe1a47b","datavalue":{"value":"Davis-Putnam procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$9C0431AA-7C64-49AF-9878-F792F8C12309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$1C191E20-C2D2-46B5-B9D4-58098BC66C7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"972920fe5cb341d56dc438d181b987ba5ef1ead3","datavalue":{"value":"random formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$EFE7D188-1BC3-4A86-924A-C8D89F3FDF34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67e20ec6afb054a049240872a3d9dccdc97f09e8","datavalue":{"value":"search algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$F51B45F9-3CDF-41AA-A051-FCBC4FD4CE25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e0192fb524376f45dfdd3eb1a809bf3cd5a9489","datavalue":{"value":"lower bounds","type":"string"},"datatype":"string"},"type":"statement","id":"Q2784492$87E03EEE-74CB-4254-8BE7-E2B1EA4411BB","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":"Q2784492$60D2F1A1-D468-4D19-ABB8-65775D072265","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"1f452ccbdc693614b6f9ab6f3300afe94eba0357","datavalue":{"value":"Q56812992","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$E39E9A87-7873-4C6F-BE31-29A3AAB2F067","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"8526b0dd880f86c60818701d82790c277027524d","datavalue":{"value":"journals/siamcomp/BeameKPS02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2784492$9B96814E-CE41-4F1B-8CDD-80484E144E04","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8187c8875d112f30a00f7281e3d099a3dccd619b","datavalue":{"value":{"text":"The efficiency of resolution and Davis-Putnam procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2784492$2DEE96C9-BCBC-4A19-A5D1-64971254AE03","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e6d27e9c44e51cd9b30063f611cd0352e58336a","datavalue":{"value":{"entity-type":"item","numeric-id":4542576,"id":"Q4542576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4352d28b384ebc3dc0e645a67dadf0e356cdfdaa","datavalue":{"value":{"amount":"+0.8787577152252197","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":"Q2784492$DD3C0B15-5668-49FF-8B84-AAA0E4A3D8C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3917e3e7fe2dc83b3de6c719e805f0e55c1c890","datavalue":{"value":{"entity-type":"item","numeric-id":5466490,"id":"Q5466490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4352d28b384ebc3dc0e645a67dadf0e356cdfdaa","datavalue":{"value":{"amount":"+0.8787577152252197","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":"Q2784492$45731FBA-0FC3-44DF-8458-4A6016156ED4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d8704fbbc5bc889cf64881a5cb2a40f7cd9e78d","datavalue":{"value":{"entity-type":"item","numeric-id":1887710,"id":"Q1887710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46ddaa88f19e317ca312e08a7beffb8709b2f548","datavalue":{"value":{"amount":"+0.8557119369506836","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":"Q2784492$39F780A8-6A3F-4DB9-8C33-46A7DF51DC61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54ff441d5f90660fe62074e8e4e7c125ba1ffa58","datavalue":{"value":{"entity-type":"item","numeric-id":2843337,"id":"Q2843337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"697146c43911e4446d6f7f39164f7b6a048269dd","datavalue":{"value":{"amount":"+0.8363202810287476","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":"Q2784492$B24842BE-8E07-4AEC-97A2-D5CE4E3D9ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28e2ce5af33dc165d9887836c40a254d4cb8025c","datavalue":{"value":{"entity-type":"item","numeric-id":5175988,"id":"Q5175988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a8fd94615e941cc98d345ed21f7be1545da61be","datavalue":{"value":{"amount":"+0.8357840180397034","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":"Q2784492$F5F93104-DD09-4A1D-9895-6B0CD289623A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2784492","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2784492"}}}}}