{"entities":{"Q3608772":{"pageid":5638678,"ns":120,"title":"Item:Q3608772","lastrevid":50592116,"modified":"2026-01-14T12:18:26Z","type":"item","id":"Q3608772","labels":{"en":{"language":"en","value":"Solving Quantified Verification Conditions Using Satisfiability Modulo Theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5523772"}},"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":"Q3608772$A1556ABC-D2AC-487F-A78E-D9B69600433C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"54f6bfe514e498e705f56e7a6294218370e9cadd","datavalue":{"value":{"text":"Solving Quantified Verification Conditions Using Satisfiability Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3608772$0A678B12-7FDF-4ED6-8F13-C7B038434BA8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"df8e60d25a4d2f4d8354f64220942d517a618a2d","datavalue":{"value":"1213.68376","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$C03BA3C0-B887-4E4C-AD0E-1D3C0601EE6E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a7a87f090d2d86ca02f137fbf6ffb98b366a8c7a","datavalue":{"value":"10.1007/978-3-540-73595-3_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$5EABBB4E-8C78-4C0F-B387-D90475AC818D","rank":"normal"}],"P16":[{"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":"Q3608772$5216FDFB-5250-4A1F-BB48-462BF460101B","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":"Q3608772$5D1F812C-561F-43B4-BB8B-692ACAA4208B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608772$92309113-9DBA-4354-A18D-5AF0FAF75CA9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a99c28302e4dd8894739792255bebe5f186782f2","datavalue":{"value":{"entity-type":"item","numeric-id":3608758,"id":"Q3608758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608772$8015859A-19A9-4CD4-B6E1-1D3A73B24827","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19a1026dd4f6172034494e7235e1c6afaf15c529","datavalue":{"value":{"time":"+2009-03-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3608772$0C7B6773-C98E-4770-88C9-895E15B35143","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$A861A7C5-8DDA-4E82-A0E5-D7DCFABB5560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$B58D24A8-EEF2-414C-91DD-973C2628E674","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ed915a56f3bfbda577ea3444283459a230de602d","datavalue":{"value":"5523772","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$07CD416A-933F-47F5-BF34-2161F4EA8B66","rank":"normal"}],"P1463":[{"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":"Q3608772$BEC2F903-E28F-427A-80CA-6DD722D0D463","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":"Q3608772$7DC2A013-04C6-4F2D-8B05-41F8FF91B029","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e9d61d7f5ba6ab06291d4e818c6457c68601039d","datavalue":{"value":"https://doi.org/10.1007/978-3-540-73595-3_12","type":"string"},"datatype":"url"},"type":"statement","id":"Q3608772$4ABBCB26-B12E-4672-8FE6-E92C7011A381","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8f6ee709d64bce3a0b0805cbb1f99e0627ecc942","datavalue":{"value":"W1569747018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608772$E3384A3A-161B-45D0-8E87-7FA063224166","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12aaa4a36bdf05dc06c575e9e83887fbf42b685d","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18f481ed6cf088aa227b2f5e62abbacc75bf693b","datavalue":{"value":{"amount":"+0.9960294365882874","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":"Q3608772$6D252B52-3933-460E-85DD-029152E10EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e71bfb5b68d2283442ce2c6ed865faa5ef3fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5756564,"id":"Q5756564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4545d1186f99030c5f9d91966e94187b9a141d18","datavalue":{"value":{"amount":"+0.8244725465774536","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":"Q3608772$21C3B3BC-07A4-446F-A914-122361D48A0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c8f57a9067c9bfb9664744fb8b5d3273f944312","datavalue":{"value":{"amount":"+0.8170342445373535","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":"Q3608772$240686B6-C9BB-4F5E-8BAC-98DAE2C9EB6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1f943c54080b27de44312af7634875e7f707904","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fee73ad822571e812b16ee1424db72979dec250","datavalue":{"value":{"amount":"+0.8161075115203857","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":"Q3608772$5A635E60-B67A-4C8F-8342-2EA443EF5D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd1c1b86d1f55b8962e4a1cb4b676d99d5f676d5","datavalue":{"value":{"amount":"+0.8061059713363647","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":"Q3608772$BD902369-5123-4A42-A21D-4111B36FC503","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3608772","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3608772"}}}}}