{"entities":{"Q5419489":{"pageid":7449063,"ns":120,"title":"Item:Q5419489","lastrevid":96171002,"modified":"2026-06-05T10:35:26Z","type":"item","id":"Q5419489","labels":{"en":{"language":"en","value":"Interaction and depth against nondeterminism in proof search"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6302292"}},"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":"Q5419489$F10D4DFA-008F-4FDD-99D8-4238E59E60CF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4d5f6ce63c40d6b4799ddb4105feefa131c7a279","datavalue":{"value":{"text":"Interaction and Depth against Nondeterminism in Proof Search","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5419489$D96491C5-FA37-47CD-B0C3-3E893217F12F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9115b26f4b6d9badc0033a0258b85309dfc29a31","datavalue":{"value":"1433.03147","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5419489$33A6EA41-90B8-4FDE-A1EA-85A3E9D5793A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0585297dee4dca63837793305c1effb1d9dfe7ef","datavalue":{"value":"10.2168/LMCS-10(2:5)2014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5419489$D0149DED-DED8-4474-992C-848067354CCC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1eb7c906224cb25d5c90b525202d2d3da1ea1cb5","datavalue":{"value":{"entity-type":"item","numeric-id":1041041,"id":"Q1041041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5419489$D812612D-3720-4C93-97C5-6FC12A3D41BD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5419489$1DD8FE35-0521-4EBA-A485-DDF6C9A5035F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7deb189b65cc3fc27b859d71d92363347a0068f0","datavalue":{"value":{"time":"+2014-06-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5419489$C3370197-E49F-4B5B-B77D-6C602F45445B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cb5140cd74a8b9fc7e1cfa9fcb1b6a1ea50d9fb1","datavalue":{"value":"https://arxiv.org/abs/1403.2628","type":"string"},"datatype":"url"},"type":"statement","id":"Q5419489$56D39DC0-7A89-4C29-94B9-9FEBF60FC012","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5419489$1D7389C1-DB68-475D-A07A-F210D12E0EFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5419489$786EC53B-E8A7-407A-A215-9C4F635E35B0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b63316523eba37a8be3ff32435a05a334c094bc8","datavalue":{"value":"6302292","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5419489$A0ED83B3-486C-4184-81C9-B859D233CC11","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5419489$AA41ADE1-E305-4EFD-9047-A2BDAF2485BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5419489$5138EAA1-CA19-443E-8682-10BCF70DEF42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ffd3928aa1fd818bc1a8806528172e266ac8bcc","datavalue":{"value":"classical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5419489$CD946B30-525B-448F-A394-3DF1568C2E3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"223100e53e73fed8e253ee46e8a2984deaf67b5b","datavalue":{"value":"deep inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q5419489$57CC0B12-F73F-4764-840C-93FFF691308C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4879e8c35d56fd297a402f7c1eba53238e04d57b","datavalue":{"value":"proof search","type":"string"},"datatype":"string"},"type":"statement","id":"Q5419489$3EE191F7-795F-4DDA-8D14-1F605B2C3263","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5419489$A1EC3617-DAFF-4A52-8797-CBA79F5E4C4B","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":"Q5419489$D42013D0-C6A5-4688-BDA7-CD77DCA11606","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01a6b2522250a718cdadbee47e44c361b68d18b2","datavalue":{"value":{"entity-type":"item","numeric-id":4645729,"id":"Q4645729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f85558932bed9d662cfd261aac2231cafe8b368","datavalue":{"value":{"amount":"+0.8492183685302734","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":"Q5419489$883B878C-2482-4269-8972-8072F48366E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4041bd2b4e07bb18d5cb36a3fdde866a268fa874","datavalue":{"value":{"entity-type":"item","numeric-id":3010365,"id":"Q3010365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8aa135c2812960c0740a34ef3e33c26f58d30e1","datavalue":{"value":{"amount":"+0.847303032875061","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":"Q5419489$B42C4EEF-958D-4CE6-A765-15159E3A8486","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6dbb346f4d6438497a93358f9fc5d941f401797","datavalue":{"value":{"entity-type":"item","numeric-id":2946572,"id":"Q2946572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e542574c584243ec8150ad6097b30a07046fef4d","datavalue":{"value":{"amount":"+0.8162908554077148","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":"Q5419489$C5460AC2-C75E-478E-A696-2E85E0DA23F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"340b90ab6436e914d85d79fe4462a4cbee5d6104","datavalue":{"value":{"entity-type":"item","numeric-id":5387898,"id":"Q5387898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51f22a82abe5ac7a35ee001379aae19ff6e53139","datavalue":{"value":{"amount":"+0.8051719069480896","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":"Q5419489$73ED3BA3-BA91-4BB0-9BBC-D05B9C3365BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70e995298ffe3a7f5c2bbf62514844ca9135cc34","datavalue":{"value":{"entity-type":"item","numeric-id":5415654,"id":"Q5415654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6d4a8171e6d350314bae480a1c54f3cf352d891","datavalue":{"value":{"amount":"+0.796673595905304","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":"Q5419489$CF90A9AE-DA04-4D27-82F2-69BE5FEF9C40","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interaction and depth against nondeterminism in proof search","badges":[]}}}}}