{"entities":{"Q5222945":{"pageid":7252515,"ns":120,"title":"Item:Q5222945","lastrevid":91613651,"modified":"2026-06-04T23:37:25Z","type":"item","id":"Q5222945","labels":{"en":{"language":"en","value":"Function summarization modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7076861"}},"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":"Q5222945$16A32FE0-BF16-4665-A979-F17CCD68BBC9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5805676c0dfbf5f5ded1f546d50ac840e9b0d025","datavalue":{"value":{"text":"Function Summarization Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5222945$65FD7712-D36F-46A9-8031-6D2C4B111213","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f6bd820ace6a57f8707a2c281d92dd14e986ca51","datavalue":{"value":"1415.68141","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$D1069468-F92A-4A94-811E-234D216D55ED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"15e7c1aedd1baa324b672c3101ff381befec47d1","datavalue":{"value":{"entity-type":"item","numeric-id":1629958,"id":"Q1629958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$5A322F9F-696E-4A88-AB1D-87EE3DA96454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0946a618bb46938edb68aaca49138b9212c6eb14","datavalue":{"value":{"entity-type":"item","numeric-id":784137,"id":"Q784137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$1793C377-3CA9-44B6-855A-4033FDB9D8AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"138e91d832e835b45e439ed8c45f97cc7963138e","datavalue":{"value":{"entity-type":"item","numeric-id":784130,"id":"Q784130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$72FA20F2-7E33-42EF-9181-C78391D9EFA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ebfd430f823a6478294286ff8c6d38b91b1861a","datavalue":{"value":{"entity-type":"item","numeric-id":784138,"id":"Q784138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$CF79016C-CF43-4B69-8269-3C7FF7A204D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42837484d31cf34ae729e1df3cf49a1e2bca3f05","datavalue":{"value":{"entity-type":"item","numeric-id":1629957,"id":"Q1629957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$4B172C4C-B51F-4AEC-BA22-4E4AED7EE877","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"66a480d2e9b29ea82a9b0fc72873fd6d8201d31c","datavalue":{"value":{"entity-type":"item","numeric-id":287271,"id":"Q287271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$4E47B927-6198-4FDC-AD28-D34F5F14EC01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a7855d416a438be572c6a7aefce1c905376fea9","datavalue":{"value":{"entity-type":"item","numeric-id":233000,"id":"Q233000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$44AC09D8-BA55-48D8-B782-F3DCDCD569A1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5222945$0A746765-77E2-4FF2-A000-49389D664DCF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"311afef0a4b95245df7f6c2908ad6e9d40f3f2be","datavalue":{"value":{"time":"+2019-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5222945$75701848-479A-4B85-820E-CE3D1A2F554B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$96DC3A8C-4C05-41F5-8D6D-E88EF0ACF596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$05BA66E0-F993-4F4A-95A1-19702A21370E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b6ad7a3c99972b386157ad015c635f82e6fe54ba","datavalue":{"value":"7076861","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$329F5DDC-7266-41FF-AA88-9CB04BE22FB3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$C70E746D-2F9A-40C4-8456-126303D574CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03f1ce721ffa5b2f36084f57048f17032077e128","datavalue":{"value":"Craig interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$DF3A30E8-2A1B-4FE5-8388-70F7FA484F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f421fe846d7b93c22df7f69976d34543b6943770","datavalue":{"value":"function summaries","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$3372BC83-33C1-42FC-8E32-BA70EF707392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c86bbb0ed08182278f2f2e406879bf596e0992c4","datavalue":{"value":"incremental verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$B27E29C9-05D0-4B9B-AC31-0D448CAEB109","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$F72DB929-71D2-48CD-A72A-D7EEF71CC81E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5222945$F06BD107-3E3F-47DD-89AB-43BF30502322","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":"Q5222945$66B34B88-C60F-4882-8C81-C29840FB533E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"252055407642a7d49532b0b6acdb7469d1423748","datavalue":{"value":"https://doi.org/10.29007/d3bt","type":"string"},"datatype":"url"},"type":"statement","id":"Q5222945$A1379B8A-69E3-40D6-8A81-AC81E9EB46A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2fd08a6331395666c3a6382b93f54d47292fa6a3","datavalue":{"value":"W2900845427","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$CD869C2B-6FF4-438A-8462-3D9756933479","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2392b96c35bc9742cce6971ccc05a9a405095444","datavalue":{"value":"10.29007/D3BT","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5222945$1848B8AD-19B8-41F8-982B-7DE25524B5DE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee785b8bf0751d66abea2867edda087f6ad28a43","datavalue":{"value":{"entity-type":"item","numeric-id":1680264,"id":"Q1680264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cde2b41b945c28bee89551b60eb03cc2ab01c3f9","datavalue":{"value":{"amount":"+0.7723779082298279","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":"Q5222945$D0A66DCD-6EC9-4F03-8714-183C7143F9CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95f1aeced5614af143a642f3f63045a54698f4a2","datavalue":{"value":{"entity-type":"item","numeric-id":2234080,"id":"Q2234080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91559f8c5f939830421088bda235b2f3738f0980","datavalue":{"value":{"amount":"+0.7191216349601746","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":"Q5222945$E47105CB-7239-479D-B45C-A5912477E285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72f2beb968a92a8234db0e3ae391703a42c99f5f","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1778182b661fb00d5b6e47befe9f2c070de086ae","datavalue":{"value":{"amount":"+0.7170981764793396","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":"Q5222945$5AEF1B51-933E-477C-8C72-563A62794EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d368107344918cf344e91551289f3ea49aa9f173","datavalue":{"value":{"entity-type":"item","numeric-id":3189836,"id":"Q3189836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a9305b87c2398dc1e23381455931d888d0cb33a","datavalue":{"value":{"amount":"+0.7111927270889282","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":"Q5222945$A4A09D98-242F-4847-AF99-1CCC817E6964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e7efe3f01bdfd05a10577c3e89926fa8a48ca69d","datavalue":{"value":{"entity-type":"item","numeric-id":1703012,"id":"Q1703012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36a7bea6ac6a6517777cbf3efda9cfd4394715c7","datavalue":{"value":{"amount":"+0.7087912559509277","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":"Q5222945$E8CB1E6E-94D1-4550-9C1E-EFEC5A8EDF58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Function summarization modulo theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Function_summarization_modulo_theories"}}}}}