{"entities":{"Q2848690":{"pageid":2859410,"ns":120,"title":"Item:Q2848690","lastrevid":51834728,"modified":"2026-01-20T06:53:09Z","type":"item","id":"Q2848690","labels":{"en":{"language":"en","value":"Integrating a SAT solver with an LCF-style theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6212136"}},"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":"Q2848690$E4E3211C-0588-4723-948A-9C07E5A661A4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"26cd5524d8002a3825db286560a880f8daa3cf2d","datavalue":{"value":"1272.68366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848690$2E6C7305-0FAA-47E9-B2F4-170F3E4DF62B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1f8cd3b806fd78547b3f4844ba487e41a5ec455","datavalue":{"value":{"entity-type":"item","numeric-id":286783,"id":"Q286783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848690$441F838E-BE80-42E8-BB03-3C801D2A62BD","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":"Q2848690$4A290633-C649-4CC3-857C-ECF0C7BF448C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"566009cb684b48422b8388cc5a8356c3dbf1360d","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066106000089","type":"string"},"datatype":"url"},"type":"statement","id":"Q2848690$665BC8F4-AEAC-44BA-A415-DE85AEB4ECE1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848690$EA67B171-C61A-4D44-B74F-EB429E4392B3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ad79804b7999ecff68a3cf2d174739a1e6aeb6ea","datavalue":{"value":"6212136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848690$0647E2E0-9BA2-4897-A92E-47CB101FFDFE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848690$9AE6DEF3-F057-40A1-94EB-7E64F88BAF1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af3b5ddb4818ec81bb9bea3bab4852742bff1bd5","datavalue":{"value":{"entity-type":"item","numeric-id":22101,"id":"Q22101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848690$2A4E3D7B-2F87-4B2E-8DDC-29CE16A945DD","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":"Q2848690$612BD85E-CFBA-4551-962C-2AE234D909F5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e245b8af8e618b2f97412fe41db1f4b843372c40","datavalue":{"value":{"text":"Integrating a SAT solver with an LCF-style theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2848690$011ABCA7-DC2C-46E6-9F15-8E88D4E10623","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab683a7b1f35576127c529e6651dcc1403e6eaef","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a54eb53319b60f43ab680d6f483c1e75c6f5ec8","datavalue":{"value":{"amount":"+0.8999114632606506","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":"Q2848690$3A2AAFAD-6536-41AF-BAD7-9D1ABDACA63C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2be33ccab093ca2a6b6fd2b7057b69ca7524c000","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5226d75feddc750eb29e61ea667d68f0dcd7d42f","datavalue":{"value":{"amount":"+0.8113531470298767","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":"Q2848690$048BDB5A-643C-4432-BF54-B50B40224F17","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":"73658c43f273295974fdfe6f7068e29aaba2296f","datavalue":{"value":{"amount":"+0.7779602408409119","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":"Q2848690$D42F92E6-212D-4AD8-B879-E8AE52E5F13C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e434c6f686246887cde238823958ad79571304c4","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6fa0c2394cbc776812adfd82c7352b16178f6e63","datavalue":{"value":{"amount":"+0.7719361782073975","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":"Q2848690$21156E31-3610-41AC-BFE3-7413B74C1EEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b4f75f494f6421c325356fd1ed820027bfc297a","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1a0763699f6e43bc42779bad87caa6fbb8889b9","datavalue":{"value":{"amount":"+0.7706871032714844","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":"Q2848690$75618B5F-49C3-44E8-860E-838AB34310AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2848690","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2848690"}}}}}