{"entities":{"Q1037401":{"pageid":1039249,"ns":120,"title":"Item:Q1037401","lastrevid":50822666,"modified":"2026-01-15T07:37:50Z","type":"item","id":"Q1037401","labels":{"en":{"language":"en","value":"Solving quantified verification conditions using satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5633345"}},"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":"Q1037401$AF25FDC1-DFCF-45ED-A18E-D2E846A4ADE8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ded9f7c77508ffdca7da924a946bb948ca146155","datavalue":{"value":{"text":"Solving quantified verification conditions using satisfiability modulo theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1037401$BC894485-7B33-4C33-A944-A2A09907700F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2bcfe72d5ed37e43d31402a4fe0fa3bb44c90d50","datavalue":{"value":"1184.68461","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$B4A42DC0-6868-4ABA-94DF-8BD28D962E26","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":"Q1037401$DBC46430-F886-4FCD-A796-6E3E59900995","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":"Q1037401$B22CB903-275E-4672-B8FA-A26ED8986E55","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":"Q1037401$8080EB12-316F-453B-88BB-586B38A7C2D2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7346dc34d1d50fea46ec345fbc7e3214530889ab","datavalue":{"value":{"entity-type":"item","numeric-id":276517,"id":"Q276517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$20D92DC6-44CB-4D2F-B3C2-A3F016BE45D3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a063ddf8a89ca70cf9f598d7256c305bf346c0e5","datavalue":{"value":{"time":"+2009-11-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1037401$49DAFE2C-01EE-42B5-A775-9DFB20DA9048","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$0EC9FD1B-7BF1-4D08-A4B7-8B95AD608310","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$BC7C113B-3A5E-4FF7-A923-7BF79FE3859B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$081D2D94-5FB3-470F-AC3E-0FCC5D7947C9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ef6a5a864fddbeb83a20417195f01277e7431f60","datavalue":{"value":"5633345","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$456C0501-3106-485B-B8DE-F6D7CCA2B2C3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b54a6cb30268c2418ffc5b80b831f9943211d1e","datavalue":{"value":"first-order automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1037401$A315DFC8-B06D-442B-B189-895BE48065A7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$0C12F873-FBD3-4D4A-BB3B-ECDAFCF94A40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a2e4454b50103c6e6499c664726a4f18fc7c5af5","datavalue":{"value":{"entity-type":"item","numeric-id":16784,"id":"Q16784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$BE9FFEED-61C9-4C6F-83D3-5E0415EA630E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$DB73B7DB-5F5C-4683-8BEA-C61F558A7C74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$CC046131-68C7-4F30-BEAA-9CF6EB682430","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":"Q1037401$BA60870A-512E-4EBD-971E-13858562DC0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$88315729-B842-4FD1-9E20-F3DD0B3D6CBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$780FA781-906B-426C-AACC-F7583D948F8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$FE4E7C11-B0EA-40A7-A31F-90EE137BFB32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8312fa7309b2bb86919d80d9dd327b01ccd3eb19","datavalue":{"value":{"entity-type":"item","numeric-id":19268,"id":"Q19268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$4F6238CA-7213-49B9-B943-C3EB1FD046B6","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":"Q1037401$9DB83B46-CA93-4623-8D63-B377890531ED","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc3af3d7b585aa63e47021ec96a23d0ee0cb5500","datavalue":{"value":"https://doi.org/10.1007/s10472-009-9153-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1037401$721EB3EE-31B0-4D10-994A-BF12AB978B00","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c7a2fffc45e1061c4c5bf8c696cca66022723b7f","datavalue":{"value":"W2009715851","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$DBE183E9-A59D-493B-AECF-CEF0814062C8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a351897245977aa0d098a2219b09f6d20cfa230","datavalue":{"value":{"entity-type":"item","numeric-id":2751360,"id":"Q2751360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$CB41F771-8A04-4226-8F8F-75E392D2D458","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14bd97e9dec390545916db4e89e737371beca26b","datavalue":{"value":{"entity-type":"item","numeric-id":5387916,"id":"Q5387916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$D45107B5-1E91-455C-82C0-756A60117688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c10bd59885420c4841d56d098f27b4158c1d680","datavalue":{"value":{"entity-type":"item","numeric-id":4737130,"id":"Q4737130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$05A7D857-A4A2-4098-8053-E451EFA915B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac1293c449a4ec199dbf2381bd6d081ce1eb4f43","datavalue":{"value":{"entity-type":"item","numeric-id":2389629,"id":"Q2389629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$266C2C28-6F28-4FBC-8D02-BC7123D30CEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$A542347A-6841-4C53-A539-A6B585DE57D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3a25e9311f149db16764369e47282066b24774c","datavalue":{"value":{"entity-type":"item","numeric-id":5307058,"id":"Q5307058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$59930BE2-8C98-4B8C-A565-ECD7F08DB797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$6FFB14E0-D7C9-4216-8402-E322B934AAF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da96dfa99f70c6b2b69c48b417a516b8fa851830","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$DB534698-3149-49D6-8AA3-AAE8E9CD3792","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"863e4781dcf0a2a9fe02df51636e0f8bb63376f0","datavalue":{"value":{"entity-type":"item","numeric-id":1610676,"id":"Q1610676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$C60AFF5E-D03E-4C5D-86B4-1DD4783527B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4d8e42945beda42154d7aec024ac2937b8249c","datavalue":{"value":{"entity-type":"item","numeric-id":2864401,"id":"Q2864401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$3D17950A-8D3E-4AE4-A726-1B0C32B1DE63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f00589542fdb6ec4fc401e47318165d5bad4f817","datavalue":{"value":{"entity-type":"item","numeric-id":1581853,"id":"Q1581853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$E524342A-D34A-441F-B469-11EB4663E270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$59B8F396-C3CA-42FE-9FF4-E9C8937BC030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$E8619C75-E787-42CB-A523-8334B02B1F11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037401$FEC20D43-D596-4A92-9134-5E1E016D9B84","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3cb68cb68c79ac5e030fb9dcdb94051c831e968d","datavalue":{"value":"10.1007/S10472-009-9153-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037401$0A04C6E6-7CAE-4729-BC39-F0C88F48B32B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9390b4ccc6dc9f08d9ed8cd2d7f1eed1c352e9ee","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"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":"Q1037401$059BFAE0-97C9-4E78-94E6-C0C2D500B0A3","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":"1ec18c7ac0d8e9f32953a6bdea5cad0a104673c1","datavalue":{"value":{"amount":"+0.8217862844467163","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":"Q1037401$C7766DC4-6AFC-4E32-AEFC-04D5603FDD13","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":"fd1c717316c80e0a6879c2efef7b864ccf301e52","datavalue":{"value":{"amount":"+0.8175261616706848","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":"Q1037401$0A86088B-9FB6-43D1-A963-73DF04D7A8F4","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":"3dc45d16ead2e9ce24ba6e79c05e900687551566","datavalue":{"value":{"amount":"+0.8127787113189697","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":"Q1037401$8BC38818-50F7-474B-BABF-DC15C60FBA8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"709211d935c435620f867d257bf161ec3a85cbd6","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24233ff3caa6fab8302e07d0d8b453185606947f","datavalue":{"value":{"amount":"+0.8088380694389343","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":"Q1037401$E7F5D345-ECEF-43DB-8CF9-B9DBCF5BEBBE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1037401","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1037401"}}}}}