{"entities":{"Q2926657":{"pageid":2937377,"ns":120,"title":"Item:Q2926657","lastrevid":52122419,"modified":"2026-01-20T23:51:14Z","type":"item","id":"Q2926657","labels":{"en":{"language":"en","value":"An abstract interpretation of DPLL(T)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6363648"}},"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":"Q2926657$A9A975DC-875D-4AE6-B3B2-934D8A1E7648","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8384b981146fe5eb8ab28f78a22fcdaaacf6ef9a","datavalue":{"value":{"text":"An Abstract Interpretation of DPLL(T)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2926657$B08F21C4-7039-4E53-9119-60432072BDF0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0ce438674e2f443050a6e59a104dafa1bb97b874","datavalue":{"value":"1426.68249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$AC2A139B-4B02-4258-9FFA-57ACA4CC3847","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bcb29fc7485cb02fb21fcd0cd15b3c1099f3c3bb","datavalue":{"value":"10.1007/978-3-642-35873-9_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$EB35601B-7FE6-40E6-BC79-69D16C4BE62A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f9ecefe21c6ae876627103481238d3a51a19d6a6","datavalue":{"value":{"entity-type":"item","numeric-id":479833,"id":"Q479833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$3B6A433B-EBA0-45CF-AA29-1C2C7885A4FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"14a0eb23269ec1fc8704436b597276cf095d31ae","datavalue":{"value":{"entity-type":"item","numeric-id":479834,"id":"Q479834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$2326F03D-AB1E-4D8D-80FE-3F416CF0052E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d3f434bb92565e5cf6d2b60aac0245f4a58be6b3","datavalue":{"value":{"entity-type":"item","numeric-id":479836,"id":"Q479836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$8549867C-B168-48C9-9E1B-8654953DA0E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$567EC6F2-3373-4418-BE40-6EEA74947026","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"de4a775b741b129661b3807102896dab39bea660","datavalue":{"value":{"entity-type":"item","numeric-id":438554,"id":"Q438554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$1D665293-D9B9-445C-8DE1-303862FF1C98","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2926657$2E3B30C3-BA66-4C4A-8E59-F31DE8720923","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3daa83eb5c9d67846bd0433e54bd3c467e1d5cf9","datavalue":{"value":{"time":"+2014-11-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2926657$ABB8274B-FD8B-40BE-866D-7A25706EE091","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$E87DE66D-A5AA-4161-8DDD-3510894D7707","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$5D44FE22-9663-4606-8CAF-14A8BB3B49AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"56406d21cf2a6ccb4f5f6947249d458becc92b14","datavalue":{"value":"6363648","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$3F0552A2-6A1D-437C-94D2-2E9F6549EFEE","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":"Q2926657$AECAB1A9-4A6C-4CFC-A08E-E93AB88D0474","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"11330083cb3ab6b838449a225f8910e1abc4a66e","datavalue":{"value":"https://doi.org/10.1007/978-3-642-35873-9_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q2926657$10EC79D7-8611-461C-AC11-4324FD71F889","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5adc250690c3b4f85cd5e1ae8bfcfdc267d7bc02","datavalue":{"value":"W2099272825","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2926657$863809D7-677A-4534-B5AA-D8D8CC8ED7FF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad4a777bf0bb99053f551e2b6fa0361d1c8156bb","datavalue":{"value":{"entity-type":"item","numeric-id":5705940,"id":"Q5705940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0741aa649ab0f9b84a2848ebc6698026f49be914","datavalue":{"value":{"amount":"+0.8687675595283508","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":"Q2926657$503404E1-B822-4B5E-BDE2-D1B3DE2F0E6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbd1f875057910272dc1f6cefa7437b5d6cd54c8","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"547649e1151fb3ce7eca48f4df28708a8caac519","datavalue":{"value":{"amount":"+0.8572476506233215","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":"Q2926657$651588FF-51A4-435E-88ED-F20443E4C447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abae2632032a03fe360c1a3290fc2dc2b9b0dcb1","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a89a99b67a6ec1f9b6e345f4da526077a74f914","datavalue":{"value":{"amount":"+0.8007379770278931","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":"Q2926657$76544BF5-CB24-4FF2-AF0E-7D2EDDD64DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47227c3ededf306d0bae5b081c3c2eaf0e20bdbf","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"41e4cfa5db4a00537578e6337b969a6376b8d99c","datavalue":{"value":{"amount":"+0.7959104776382446","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":"Q2926657$6FA1B3AB-65B3-4ABF-8126-F9C0E4C0339D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f73ef4e4cd40d6dc34268d177258481051eb4b8e","datavalue":{"value":{"entity-type":"item","numeric-id":5716574,"id":"Q5716574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2f440de8097ec412dde58f771f6bcf4b7162750","datavalue":{"value":{"amount":"+0.7924408912658691","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":"Q2926657$5ACE7BDA-2EC0-409D-B6FC-9F777BE82A97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2926657","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2926657"}}}}}