{"entities":{"Q989569":{"pageid":991417,"ns":120,"title":"Item:Q989569","lastrevid":65866161,"modified":"2026-04-12T05:54:48Z","type":"item","id":"Q989569","labels":{"en":{"language":"en","value":"A simplified way of proving trade-off results for resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5773848"}},"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":"Q989569$3C7D2DAF-4807-43A6-ADCD-A12628AA983A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"59fb34d601a85098bfdc9c042327144308a19cc2","datavalue":{"value":{"text":"A simplified way of proving trade-off results for resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q989569$9B8E76FB-3F82-4A71-B4F7-E6D21800D852","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3329f0f242a22cfe513b9bcb256651e3a2a74daa","datavalue":{"value":"1202.68388","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q989569$09CFCAC9-BB94-4F62-9692-2ED328397EDB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7ade4990ab7a79bdd900e48d3fab8c751fcf8949","datavalue":{"value":{"entity-type":"item","numeric-id":989568,"id":"Q989568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$6A186608-CED0-42BD-9FB8-6311D2F1038B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$B1A65595-9A69-4750-B5E2-E8E6C5DC0BF8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eca87747cfd61cbf3bdf39bd7734ed4289af3510","datavalue":{"value":{"time":"+2010-08-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q989569$4DE06A48-C3A3-4462-B85B-2A20B1BA46DA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q989569$BE3DDA9A-7A93-426E-8E95-44525E093AF7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"559426ef26847d96be9378aea6e13e6497e9c69b","datavalue":{"value":"5773848","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q989569$5CF1728D-20FB-4842-9569-276DE2071CB5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ba0cc3f7aaac8445724ef309c9eecb57f5a563d","datavalue":{"value":"computational complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$08D403E2-9660-4AFD-B8BF-0E87907E8505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$DF4FD445-935E-40A0-B344-FAA865483B21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$D216CC5F-337A-406C-80A5-06DC746EA83A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$9298E894-D688-4806-BB3C-642C403DD654","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a0b9e816c430cd3e88ed419c55803a9d678ae625","datavalue":{"value":"trade-offs","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$FC07E606-6DBF-42E7-8CFE-9D749EC373F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4aa90b1ff0982ab5d5fab48275d3f9dc7c1839ee","datavalue":{"value":"length","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$84DE24A7-2C39-40C9-B33B-2384D8DC3504","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ccdf98bea6de3dcf3a7edd1fca9d3b62359e75d8","datavalue":{"value":"width","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$C73B5024-7244-4296-99AA-12D79E0D6059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73a97cccd1f884fd46602d4e8a0ed129e1fea3bc","datavalue":{"value":"space","type":"string"},"datatype":"string"},"type":"statement","id":"Q989569$5D41726C-F39B-44B5-81F0-283F81BBA472","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":"Q989569$AD299CD4-6D21-47A8-B36A-974172C68205","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4203a471e7b78be8c2b901da741dd58f0482b314","datavalue":{"value":"https://doi.org/10.1016/j.ipl.2009.06.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q989569$9AB59B5E-94D5-46E4-9EDB-6DB31449503A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"22ff5d2893b0bdc42958c17f52bc9922a16da77e","datavalue":{"value":"W2109895531","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q989569$A995D3D4-E0C0-4BFE-8504-1CE00A96B687","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ff8a1d983dc735fd82f262f00fed618f4232eaf","datavalue":{"value":{"entity-type":"item","numeric-id":3149864,"id":"Q3149864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$37DD0836-780A-4F8E-B4F9-DD53B35351B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e608320df31f8e48c84ddb3e288d0df61ecac3d","datavalue":{"value":{"entity-type":"item","numeric-id":2475405,"id":"Q2475405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$356AAE88-97DF-49A6-8820-261D4B7871DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"845eaabfed9368451854349c91bbdb46d85b1f07","datavalue":{"value":{"entity-type":"item","numeric-id":4417005,"id":"Q4417005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$E2B07261-8DD1-41CB-B941-12A62C59B6E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b529296035947435eb136154e374f9657d895b","datavalue":{"value":{"entity-type":"item","numeric-id":4406287,"id":"Q4406287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$3BBCE7B3-EFEF-465A-BC20-990B53B87E1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34354019cc1f4775fba2a3965f1a17955115f4bf","datavalue":{"value":{"entity-type":"item","numeric-id":1405735,"id":"Q1405735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$867AE8ED-F174-41BC-A2B4-85E1EE4C8D65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c55ef7e4f75a570fef930a1f823c7040905ef92","datavalue":{"value":{"entity-type":"item","numeric-id":1854472,"id":"Q1854472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$E89FABA2-082A-4CB8-9625-B4A795E8D158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0b6745e2bf83540023384ad2f4a2cc1400adfe3","datavalue":{"value":{"entity-type":"item","numeric-id":5189540,"id":"Q5189540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$249AC85F-57A6-486D-A656-710464A700AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ced61c84792450b85b0d481b502b86f0bde2b7f4","datavalue":{"value":{"entity-type":"item","numeric-id":5302095,"id":"Q5302095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$C45DB3E0-EF22-4A19-883F-CBFAC59C767E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"458ab467d1c5397109a383d0e5c939369d06a212","datavalue":{"value":{"entity-type":"item","numeric-id":3221403,"id":"Q3221403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$49DA60D3-9401-4AA9-8E02-56409CD5F190","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ebf50b3b231b28dd36b98369bafa45d547ad97d","datavalue":{"value":{"entity-type":"item","numeric-id":1109565,"id":"Q1109565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$0426C44B-DAD3-46F2-BE26-5097733DF881","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd67cf9cc8c3a39ebb38f217a93e786c313e8d48","datavalue":{"value":{"entity-type":"item","numeric-id":1924995,"id":"Q1924995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$9B42A18F-1F4A-42A5-839A-ADC3DF27BE89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bda20905c77d3e8a02baadccc76bf3fc2281d82","datavalue":{"value":{"entity-type":"item","numeric-id":4945238,"id":"Q4945238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$C4D56770-DB92-4038-8479-BD1AD19C87B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q989569$EE6D0E44-E6EA-425F-A986-05599CA5C28C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0ba6ddf58d23ef47228574d87226c286a3db0620","datavalue":{"value":"10.1016/J.IPL.2009.06.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q989569$5ABA869B-DA76-4115-B1EC-A1040BA6C431","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4081d2a0215b083c4262ab1d473dfcd8460929cd","datavalue":{"value":{"entity-type":"item","numeric-id":3654387,"id":"Q3654387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0e910bfd158b695b0940c3feaa893dd092e5a81","datavalue":{"value":{"amount":"+0.802643358707428","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":"Q989569$8599EC8A-AE21-4450-8905-E0A4E4EA6D9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5856dd7dd9ddf199bc9d04e5efadc38ade5f7526","datavalue":{"value":{"entity-type":"item","numeric-id":2816413,"id":"Q2816413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd10e8b922247567f397e9bbd4457353b160af27","datavalue":{"value":{"amount":"+0.7910881638526917","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":"Q989569$780335A4-0582-4281-9984-D4B80377AB73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88487d39d860afa32f6d456fc8042ed67d952460","datavalue":{"value":{"entity-type":"item","numeric-id":2817796,"id":"Q2817796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8e074450177ac2c070d22f580fcd1d51d6c06ae","datavalue":{"value":{"amount":"+0.7904167771339417","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":"Q989569$6189D246-13EA-4EA4-8D8A-0BF993B2A3AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"070cacf0f29221af8e07f77a8c0c4d6ff7eeb031","datavalue":{"value":{"entity-type":"item","numeric-id":1616620,"id":"Q1616620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89ddf4bc163c977380c9fbcff2365f5c529742ca","datavalue":{"value":{"amount":"+0.7861692905426025","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":"Q989569$331843AA-30DB-4C31-B4CC-A0B2A222E8C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7401c2396678df9562b830016a74a99eb6540cfe","datavalue":{"value":{"entity-type":"item","numeric-id":4598196,"id":"Q4598196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5c86b428ac5b9b7022bee4bda08d1d5b1457cb0","datavalue":{"value":{"amount":"+0.7860831618309021","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":"Q989569$8D4452BF-F454-4278-AB36-25F6AB0688BA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A simplified way of proving trade-off results for resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_simplified_way_of_proving_trade-off_results_for_resolution"}}}}}