{"entities":{"Q2848688":{"pageid":2859408,"ns":120,"title":"Item:Q2848688","lastrevid":51834719,"modified":"2026-01-20T06:53:09Z","type":"item","id":"Q2848688","labels":{"en":{"language":"en","value":"Cooperating theorem provers: a case study combining HOL-Light and CVC Lite"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6212134"}},"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":"Q2848688$17E7E3CE-8423-4CAA-976E-AA94BDE8C7A8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"126d475617c794d0d6be47614b5ee491162c8e66","datavalue":{"value":"1272.68362","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848688$F541BA88-DF41-4066-8639-DF6142229513","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"77ef26b195160569d7e65188fa689f9dd610af9e","datavalue":{"value":{"entity-type":"item","numeric-id":2225087,"id":"Q2225087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$A48211E3-603A-4EEE-B4CF-D892F5757B63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$B2417586-5896-46F5-A6DD-CB53F9334FAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"747ef58d5282c7c6e14680778d7246c63bd5b0fe","datavalue":{"value":{"entity-type":"item","numeric-id":1037400,"id":"Q1037400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$CEAE86BF-AE75-4FC9-B71C-3C1CFBB3E8FD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"43e878d8f753446abefa1b1ceb0637b91afae47a","datavalue":{"value":{"time":"+2013-09-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2848688$C72B359A-2F6D-4327-BD8E-B0BCB1C41447","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ad13b48120f5a41e63ccdd1f36cd62304dcdbb46","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066106000065","type":"string"},"datatype":"url"},"type":"statement","id":"Q2848688$704DEE70-CE6F-4783-A037-973AC83300FB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848688$37F23D2C-F916-41A5-B3C5-FF1B9D5E4CD4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f60087c15b73ab33ba71bdbf332039741495d017","datavalue":{"value":"6212134","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848688$89771C21-E94D-48DC-B359-3745A2CF1213","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$574C84DC-F6C9-43A2-9CA9-25F6E60DF1E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$CF41AF98-7725-4BBF-A78A-B23A8E112513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$C9A91CC8-3B47-4139-BCD8-633E5DA74294","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848688$8727EF92-6B99-4B72-9B8F-F66EBCF6AFB7","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":"Q2848688$5BB5DEBA-175F-4AD3-8D1D-7A2B4AC177F8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a61d09d4753a419566deb2e2e647d38badcedcc6","datavalue":{"value":{"text":"Cooperating theorem provers: a case study combining HOL-Light and CVC Lite","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2848688$C039D26C-C87C-499F-8FFB-54466DA6F157","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5240345605b6df958dc529fb8dc1a54b30d31b3","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82b32a210fcb24dc906ea12c60e7c40ca4038e05","datavalue":{"value":{"amount":"+0.7868560552597046","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":"Q2848688$DEBC3CBC-1833-48CC-A9BB-A995D7803118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9666d9095ca892169a9512aee8dbcd8fbe4f61","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fae59eaca59f09cdd32f4da1cadad0d4aa29a58a","datavalue":{"value":{"amount":"+0.7638901472091675","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":"Q2848688$96F2388F-86C2-4057-8EC5-698F60B650A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f4a52d9a5fcd5fdd13614de2b175a7c374f41fb","datavalue":{"value":{"entity-type":"item","numeric-id":1687726,"id":"Q1687726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2af9121925850810a0e8281edea910e94c6255d6","datavalue":{"value":{"amount":"+0.7468392848968506","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":"Q2848688$19971036-D9C2-439B-A3A3-ACAE36B35154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5331744dbaa081b115ce6275e5ee79d1d58f6931","datavalue":{"value":{"entity-type":"item","numeric-id":5705938,"id":"Q5705938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71149f527216c6e8490ea24897356be4bf29ae28","datavalue":{"value":{"amount":"+0.7456222772598267","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":"Q2848688$4380EC87-CBE8-4B0C-B2D4-EBBDC3857E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecaa33f59d7da2d63f62f7085605bb6ffbbf5115","datavalue":{"value":{"entity-type":"item","numeric-id":3088006,"id":"Q3088006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5577b3559406598c64bc47a277b176a7aba37ff2","datavalue":{"value":{"amount":"+0.7447293996810913","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":"Q2848688$B2B2C286-69C5-474B-8A63-D4BF1977709C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2848688","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2848688"}}}}}