{"entities":{"Q582116":{"pageid":583883,"ns":120,"title":"Item:Q582116","lastrevid":62948856,"modified":"2026-04-11T09:11:16Z","type":"item","id":"Q582116","labels":{"en":{"language":"en","value":"Refinements to depth-first iterative-deepening search in automatic theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4130039"}},"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":"Q582116$8B00B338-A806-41AF-9BC4-CE912AF34E27","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c66aa57ee22cf33dea72dc7255dea26cdae738d6","datavalue":{"value":{"text":"Refinements to depth-first iterative-deepening search in automatic theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q582116$17814A38-4489-490D-B111-39EA3A34B280","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8214cfb85f9063418a70badca689dc3cea1e5679","datavalue":{"value":"0689.68087","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$222B34B0-6297-41FA-9217-036222B33B7D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6b2e333005a695ac088694de439f8c4a2c93b8e0","datavalue":{"value":"10.1016/0004-3702(89)90011-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$211377F7-0EC5-4D40-914D-4129BB963B0A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0b6721df2a0037b15fd86f65472c88ec7ecc0ce5","datavalue":{"value":{"entity-type":"item","numeric-id":582115,"id":"Q582115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$626CB636-0B5C-4C5D-8BF1-EFB9642B9B21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"34f99c9947f4d98af9da609b6496b55645bbe075","datavalue":{"value":{"entity-type":"item","numeric-id":1238600,"id":"Q1238600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$D9E4FDA4-827A-410A-9C05-237379E294CD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$69EF7947-BD27-4D62-8FF2-F6BA2DA0E842","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q582116$ACAFB9B5-17D8-4699-AD35-8E2075ECC0B8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$9AAFD3BF-651A-4A70-A7FE-A05F3C03EE9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$A35AE9CD-D73D-4365-BFC8-D759A51C4E26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$044214D7-0B43-44DA-ABFA-7FC72B3E9A44","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f12e7348d83233cf1b79ff2235c07c660fe6d0ff","datavalue":{"value":"4130039","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$EA962A50-6241-4628-9B06-77CD854C4288","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"31b024a2ec26ec1b7fea930464ef722f25e93c55","datavalue":{"value":"depth iterative-deepening seach","type":"string"},"datatype":"string"},"type":"statement","id":"Q582116$3875F4EC-123E-4680-800F-CF269CEE526F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a9f6ca69545d8ff62e2bbfb9e6348523e6e12ed","datavalue":{"value":"priority system","type":"string"},"datatype":"string"},"type":"statement","id":"Q582116$F6E1446C-CE8C-49AF-84AB-31357CA668D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6b948f84addd93dbc3e2d02c8d54a8d27fc90d2","datavalue":{"value":"priority list","type":"string"},"datatype":"string"},"type":"statement","id":"Q582116$3C44D0D0-5DEB-41A1-B7B3-0364B46CB478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q582116$E9CE3380-EA61-4087-9181-9A34FA1FBF86","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"219247657ba5a592ccc1993de518f5ecab5c84bd","datavalue":{"value":{"entity-type":"item","numeric-id":37173,"id":"Q37173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$D1EA9F13-E734-49BD-BCC1-6A283465D8F1","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":"Q582116$D63E04EE-10B1-4E04-B320-2A3FE6AC01D5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f2afc3577dd9adc431503324508362baa94b6f56","datavalue":{"value":"https://doi.org/10.1016/0004-3702(89)90011-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q582116$D57CEDCE-048C-4159-A7BB-CB29614BAF3B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"090fb4a3d5eb12a998c80311918386b570482e60","datavalue":{"value":"W2003493467","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q582116$10A394EC-0D3C-4DA2-B7DC-0732DE0B9A5D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"62938883e1780590c0b762bf14c5c27cf5a93bd0","datavalue":{"value":{"entity-type":"item","numeric-id":3204066,"id":"Q3204066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$BDAF9949-EF8A-49CB-B268-DE68B65C2BF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5c9250f55330f5cd1601b40853c61ae72bb2319","datavalue":{"value":{"entity-type":"item","numeric-id":1146526,"id":"Q1146526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$EC0CC987-729A-4369-B807-EA4480BFB7C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1f0b5c5d1ef7da893967c1b74defc4984f71dee","datavalue":{"value":{"entity-type":"item","numeric-id":1062761,"id":"Q1062761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$05B9A9C8-4959-4107-B94E-CA3476209B11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22d3f29968c996bb68da1f8ea593f2a057ca04cb","datavalue":{"value":{"entity-type":"item","numeric-id":5623241,"id":"Q5623241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$D112F2F2-9647-4ED6-B0B9-2B8A5C2940BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7add01291c95ebcb031afac6fc8c8b1659115c10","datavalue":{"value":{"entity-type":"item","numeric-id":1229761,"id":"Q1229761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$5B1544CB-751D-4DAD-93FA-203FEE486D27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43919d1f4da3b9a07eea3d230b3f18d880d5940","datavalue":{"value":{"entity-type":"item","numeric-id":1116717,"id":"Q1116717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$B7C7D546-045F-43E1-9341-E7B3A1020668","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$82DC46A6-3656-4E29-B7D5-F5CA7552C84A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ad23ca61534fce39d231de8434f91a2de01c5c","datavalue":{"value":{"entity-type":"item","numeric-id":1098332,"id":"Q1098332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q582116$8FA125A0-8D98-4633-BD86-FCB9D4AC594F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10e19cabe13341f67aaef2cf0b284b7eec0db861","datavalue":{"value":{"entity-type":"item","numeric-id":5419489,"id":"Q5419489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a26b0fd0e07abe679921f5ea5d3dfa6d1963f68a","datavalue":{"value":{"amount":"+0.86896","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$653E4CAC-CDDF-4013-8470-8A7D0E96F010","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30cc1ea5b7e5002bbf92c6fb2128ebdd9cb4d459","datavalue":{"value":{"entity-type":"item","numeric-id":4835513,"id":"Q4835513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3b6f93bee5310b0a6ba8b7c1aa59d93e98139e7","datavalue":{"value":{"amount":"+0.8650791","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$AEE3EC4C-36EE-4783-9C94-9CAE21D8CA9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b09c6a971b6451ef202d48aa08df2a5aabea6c5","datavalue":{"value":{"entity-type":"item","numeric-id":3709920,"id":"Q3709920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4909e8e9576c9d7771616ad173cc4343e3b53262","datavalue":{"value":{"amount":"+0.8625877","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$FC02A641-B0CF-412E-B372-F68AC56E792D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2fb232f83734a328a0e4e36b244cd2881b43d1cc","datavalue":{"value":{"entity-type":"item","numeric-id":1404980,"id":"Q1404980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5081b0a5b7c41d50991e081e934fb5e145540f3","datavalue":{"value":{"amount":"+0.8616672","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$E7D807C5-0A49-4B42-A04B-A00D10E8EF9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3328acb14c381645dbb1f9eb31b744a4a34bbbc0","datavalue":{"value":{"entity-type":"item","numeric-id":5210762,"id":"Q5210762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff47034f5094f2348970c8b4271902080bab536e","datavalue":{"value":{"amount":"+0.86078024","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$54853D2C-EAB8-4692-AA6D-54DA886647A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c365ae4452123ae097251f5b3c1589e5b0b2b3dd","datavalue":{"value":{"entity-type":"item","numeric-id":4375764,"id":"Q4375764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"616948877a9d90e3b16029a0c76b9c250fbe1555","datavalue":{"value":{"amount":"+0.85895383","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$F0747B4A-D5A5-4168-ACA4-20F746C788CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a8b950c83128d11d71296f04dbe09c8f568420f","datavalue":{"value":{"entity-type":"item","numeric-id":4928454,"id":"Q4928454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c352e148b5f0250e5bd11e59334dee6bbdbf9644","datavalue":{"value":{"amount":"+0.85873574","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$4B8E1714-C148-495D-B2EA-B76406B7A58A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b73f67e85a8f6fae8d616525462a58624976e801","datavalue":{"value":{"entity-type":"item","numeric-id":3750137,"id":"Q3750137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb592e435e9acc3c15946eb48ae6af9008443fb7","datavalue":{"value":{"amount":"+0.857977","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$90238C6E-C3E5-4111-86D3-EF6F23DDFA32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7851693d00538fb45a0e63db9591ae3b0097440a","datavalue":{"value":{"entity-type":"item","numeric-id":3612651,"id":"Q3612651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5d790a7d2890d0a37aa83f67d43be02c796e2a4","datavalue":{"value":{"amount":"+0.8555135","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$11B93211-70C8-491F-BD97-015B2B939846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe161eb90ba3769f9fc5a5b7fc17cfda6cd55c40","datavalue":{"value":{"entity-type":"item","numeric-id":3601830,"id":"Q3601830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51d23ef5319c4599feb2b648adfa9d59d6a19811","datavalue":{"value":{"amount":"+0.852996","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q582116$9B6AF2DA-BB76-427E-ADD8-0CF71D35F482","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refinements to depth-first iterative-deepening search in automatic theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refinements_to_depth-first_iterative-deepening_search_in_automatic_theorem_proving"}}}}}